Documentation

Mathlib.Order.Synonym

Type synonyms #

This file provides two type synonyms for order theory:

Notation #

αᵒᵈ is notation for OrderDual α.

The general rule for notation of Lex types is to append to the usual notation.

Implementation notes #

One should not abuse definitional equality between α and αᵒᵈ/Lex α. Instead, explicit coercions should be inserted:

See also #

This file is similar to Algebra.Group.TypeTags.

Order dual #

def OrderDual.toDual {α : Type u_1} :
α αᵒᵈ

toDual is the identity function to the OrderDual of a linear order.

Equations
    Instances For
      def OrderDual.ofDual {α : Type u_1} :
      αᵒᵈ α

      ofDual is the identity function from the OrderDual of a linear order.

      Equations
        Instances For
          @[simp]
          theorem OrderDual.toDual_ofDual {α : Type u_1} (a : αᵒᵈ) :
          @[simp]
          theorem OrderDual.ofDual_toDual {α : Type u_1} (a : α) :
          theorem OrderDual.toDual_inj {α : Type u_1} {a b : α} :
          toDual a = toDual b a = b
          theorem OrderDual.ofDual_inj {α : Type u_1} {a b : αᵒᵈ} :
          ofDual a = ofDual b a = b
          @[simp]
          theorem OrderDual.toDual_le_toDual {α : Type u_1} [LE α] {a b : α} :
          @[simp]
          theorem OrderDual.toDual_lt_toDual {α : Type u_1} [LT α] {a b : α} :
          toDual a < toDual b b < a
          @[simp]
          theorem OrderDual.ofDual_le_ofDual {α : Type u_1} [LE α] {a b : αᵒᵈ} :
          @[simp]
          theorem OrderDual.ofDual_lt_ofDual {α : Type u_1} [LT α] {a b : αᵒᵈ} :
          ofDual a < ofDual b b < a
          theorem OrderDual.le_toDual {α : Type u_1} [LE α] {a : αᵒᵈ} {b : α} :
          theorem OrderDual.lt_toDual {α : Type u_1} [LT α] {a : αᵒᵈ} {b : α} :
          a < toDual b b < ofDual a
          theorem OrderDual.toDual_le {α : Type u_1} [LE α] {a : α} {b : αᵒᵈ} :
          theorem OrderDual.toDual_lt {α : Type u_1} [LT α] {a : α} {b : αᵒᵈ} :
          toDual a < b ofDual b < a
          def OrderDual.rec {α : Type u_1} {C : αᵒᵈSort u_2} (h₂ : (a : α) → C (toDual a)) (a : αᵒᵈ) :
          C a

          Recursor for αᵒᵈ.

          Equations
            Instances For
              @[simp]
              theorem OrderDual.forall {α : Type u_1} {p : αᵒᵈProp} :
              (∀ (a : αᵒᵈ), p a) ∀ (a : α), p (toDual a)
              @[simp]
              theorem OrderDual.exists {α : Type u_1} {p : αᵒᵈProp} :
              ( (a : αᵒᵈ), p a) (a : α), p (toDual a)
              theorem LE.le.dual {α : Type u_1} [LE α] {a b : α} :

              Alias of the reverse direction of OrderDual.toDual_le_toDual.

              theorem LT.lt.dual {α : Type u_1} [LT α] {a b : α} :

              Alias of the reverse direction of OrderDual.toDual_lt_toDual.

              theorem LE.le.ofDual {α : Type u_1} [LE α] {a b : αᵒᵈ} :

              Alias of the reverse direction of OrderDual.ofDual_le_ofDual.

              theorem LT.lt.ofDual {α : Type u_1} [LT α] {a b : αᵒᵈ} :

              Alias of the reverse direction of OrderDual.ofDual_lt_ofDual.

              Lexicographic order #

              def Lex (α : Type u_2) :
              Type u_2

              A type synonym to equip a type with its lexicographic order.

              Equations
                Instances For
                  @[match_pattern]
                  def toLex {α : Type u_1} :
                  α Lex α

                  toLex is the identity function to the Lex of a type.

                  Equations
                    Instances For
                      @[match_pattern]
                      def ofLex {α : Type u_1} :
                      Lex α α

                      ofLex is the identity function from the Lex of a type.

                      Equations
                        Instances For
                          @[simp]
                          theorem toLex_symm_eq {α : Type u_1} :
                          @[simp]
                          theorem ofLex_symm_eq {α : Type u_1} :
                          @[simp]
                          theorem toLex_ofLex {α : Type u_1} (a : Lex α) :
                          toLex (ofLex a) = a
                          @[simp]
                          theorem ofLex_toLex {α : Type u_1} (a : α) :
                          ofLex (toLex a) = a
                          theorem toLex_inj {α : Type u_1} {a b : α} :
                          toLex a = toLex b a = b
                          theorem ofLex_inj {α : Type u_1} {a b : Lex α} :
                          ofLex a = ofLex b a = b
                          instance instBEqLex (α : Type u_2) [BEq α] :
                          BEq (Lex α)
                          Equations
                            instance instLawfulBEqLex (α : Type u_2) [BEq α] [LawfulBEq α] :
                            instance instDecidableEqLex (α : Type u_2) [DecidableEq α] :
                            Equations
                              instance instInhabitedLex (α : Type u_2) [Inhabited α] :
                              Equations
                                def Lex.rec {α : Type u_1} {β : Lex αSort u_2} (h : (a : α) → β (toLex a)) (a : Lex α) :
                                β a

                                A recursor for Lex. Use as induction x.

                                Equations
                                  Instances For
                                    @[simp]
                                    theorem Lex.forall {α : Type u_1} {p : Lex αProp} :
                                    (∀ (a : Lex α), p a) ∀ (a : α), p (toLex a)
                                    @[simp]
                                    theorem Lex.exists {α : Type u_1} {p : Lex αProp} :
                                    ( (a : Lex α), p a) (a : α), p (toLex a)