Documentation

Mathlib.Order.Defs.PartialOrder

Orders #

Defines classes for preorders and partial orders and proves some basic lemmas about them.

We also define covering relations on a preorder. We say that b covers a if a < b and there is no element in between. We say that b weakly covers a if a ≤ b and there is no element between a and b. In a partial order this is equivalent to a ⋖ b ∨ a = b, in a preorder this is equivalent to a ⋖ b ∨ (a ≤ b ∧ b ≤ a)

Notation #

Definition of Preorder and lemmas about types with a Preorder #

class Preorder (α : Type u_2) extends LE α, LT α :
Type u_2

A preorder is a reflexive, transitive relation with a < b defined in the obvious way.

Instances
    @[simp]
    theorem le_refl {α : Type u_1} [Preorder α] (a : α) :
    a a

    The relation on a preorder is reflexive.

    theorem le_rfl {α : Type u_1} [Preorder α] {a : α} :
    a a

    A version of le_refl where the argument is implicit

    theorem le_trans {α : Type u_1} [Preorder α] {a b c : α} :
    a bb ca c

    The relation on a preorder is transitive.

    theorem lt_iff_le_not_le {α : Type u_1} [Preorder α] {a b : α} :
    a < b a b ¬b a
    theorem lt_of_le_not_le {α : Type u_1} [Preorder α] {a b : α} (hab : a b) (hba : ¬b a) :
    a < b
    theorem le_of_eq {α : Type u_1} [Preorder α] {a b : α} (hab : a = b) :
    a b
    theorem le_of_lt {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) :
    a b
    theorem not_le_of_lt {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) :
    ¬b a
    theorem not_le_of_gt {α : Type u_1} [Preorder α] {a b : α} (hab : a > b) :
    ¬a b
    theorem not_lt_of_le {α : Type u_1} [Preorder α] {a b : α} (hab : a b) :
    ¬b < a
    theorem not_lt_of_ge {α : Type u_1} [Preorder α] {a b : α} (hab : a b) :
    ¬a < b
    theorem LT.lt.not_le {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) :
    ¬b a

    Alias of not_le_of_lt.

    theorem LE.le.not_lt {α : Type u_1} [Preorder α] {a b : α} (hab : a b) :
    ¬b < a

    Alias of not_lt_of_le.

    theorem ge_trans {α : Type u_1} [Preorder α] {a b c : α} :
    a bb ca c
    theorem lt_irrefl {α : Type u_1} [Preorder α] (a : α) :
    ¬a < a
    theorem gt_irrefl {α : Type u_1} [Preorder α] (a : α) :
    ¬a > a
    theorem lt_of_lt_of_le {α : Type u_1} [Preorder α] {a b c : α} (hab : a < b) (hbc : b c) :
    a < c
    theorem lt_of_le_of_lt {α : Type u_1} [Preorder α] {a b c : α} (hab : a b) (hbc : b < c) :
    a < c
    theorem gt_of_gt_of_ge {α : Type u_1} [Preorder α] {a b c : α} (h₁ : a > b) (h₂ : b c) :
    a > c
    theorem gt_of_ge_of_gt {α : Type u_1} [Preorder α] {a b c : α} (h₁ : a b) (h₂ : b > c) :
    a > c
    theorem lt_trans {α : Type u_1} [Preorder α] {a b c : α} (hab : a < b) (hbc : b < c) :
    a < c
    theorem gt_trans {α : Type u_1} [Preorder α] {a b c : α} :
    a > bb > ca > c
    theorem ne_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
    a b
    theorem ne_of_gt {α : Type u_1} [Preorder α] {a b : α} (h : b < a) :
    a b
    theorem lt_asymm {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
    ¬b < a
    theorem not_lt_of_gt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
    ¬b < a

    Alias of lt_asymm.

    theorem not_lt_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
    ¬b < a

    Alias of lt_asymm.

    theorem le_of_lt_or_eq {α : Type u_1} [Preorder α] {a b : α} (h : a < b a = b) :
    a b
    theorem le_of_eq_or_lt {α : Type u_1} [Preorder α] {a b : α} (h : a = b a < b) :
    a b
    @[instance 900]
    Equations
      @[instance 900]
      Equations
        @[instance 900]
        Equations
          @[instance 900]
          Equations
            @[instance 900]
            Equations
              @[instance 900]
              Equations
                @[instance 900]
                Equations
                  @[instance 900]
                  Equations

                    < is decidable if is.

                    Equations
                      Instances For
                        def WCovBy {α : Type u_1} [Preorder α] (a b : α) :

                        WCovBy a b means that a = b or b covers a. This means that a ≤ b and there is no element in between.

                        Equations
                          Instances For

                            Notation for WCovBy a b.

                            Equations
                              Instances For
                                def CovBy {α : Type u_2} [LT α] (a b : α) :

                                CovBy a b means that b covers a: a < b and there is no element in between.

                                Equations
                                  Instances For

                                    Notation for CovBy a b.

                                    Equations
                                      Instances For

                                        Definition of PartialOrder and lemmas about types with a partial order #

                                        class PartialOrder (α : Type u_2) extends Preorder α :
                                        Type u_2

                                        A partial order is a reflexive, transitive, antisymmetric relation .

                                        Instances
                                          theorem le_antisymm {α : Type u_1} [PartialOrder α] {a b : α} :
                                          a bb aa = b
                                          theorem eq_of_le_of_le {α : Type u_1} [PartialOrder α] {a b : α} :
                                          a bb aa = b

                                          Alias of le_antisymm.

                                          theorem le_antisymm_iff {α : Type u_1} [PartialOrder α] {a b : α} :
                                          a = b a b b a
                                          theorem lt_of_le_of_ne {α : Type u_1} [PartialOrder α] {a b : α} :
                                          a ba ba < b

                                          Equality is decidable if is.

                                          Equations
                                            Instances For
                                              theorem Decidable.lt_or_eq_of_le {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] (hab : a b) :
                                              a < b a = b
                                              theorem Decidable.eq_or_lt_of_le {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] (hab : a b) :
                                              a = b a < b
                                              theorem Decidable.le_iff_lt_or_eq {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] :
                                              a b a < b a = b
                                              theorem lt_or_eq_of_le {α : Type u_1} [PartialOrder α] {a b : α} :
                                              a ba < b a = b
                                              theorem le_iff_lt_or_eq {α : Type u_1} [PartialOrder α] {a b : α} :
                                              a b a < b a = b