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 #

instance OrderDual.instNontrivial {α : Type u_1} [h : Nontrivial α] :
Equations
  • = h
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_symm_eq {α : Type u_1} :
      OrderDual.toDual.symm = OrderDual.ofDual
      @[simp]
      theorem OrderDual.ofDual_symm_eq {α : Type u_1} :
      OrderDual.ofDual.symm = OrderDual.toDual
      @[simp]
      theorem OrderDual.toDual_ofDual {α : Type u_1} (a : αᵒᵈ) :
      OrderDual.toDual (OrderDual.ofDual a) = a
      @[simp]
      theorem OrderDual.ofDual_toDual {α : Type u_1} (a : α) :
      OrderDual.ofDual (OrderDual.toDual a) = a
      theorem OrderDual.toDual_inj {α : Type u_1} {a : α} {b : α} :
      OrderDual.toDual a = OrderDual.toDual b a = b
      theorem OrderDual.ofDual_inj {α : Type u_1} {a : αᵒᵈ} {b : αᵒᵈ} :
      OrderDual.ofDual a = OrderDual.ofDual b a = b
      @[simp]
      theorem OrderDual.toDual_le_toDual {α : Type u_1} [LE α] {a : α} {b : α} :
      OrderDual.toDual a OrderDual.toDual b b a
      @[simp]
      theorem OrderDual.toDual_lt_toDual {α : Type u_1} [LT α] {a : α} {b : α} :
      OrderDual.toDual a < OrderDual.toDual b b < a
      @[simp]
      theorem OrderDual.ofDual_le_ofDual {α : Type u_1} [LE α] {a : αᵒᵈ} {b : αᵒᵈ} :
      OrderDual.ofDual a OrderDual.ofDual b b a
      @[simp]
      theorem OrderDual.ofDual_lt_ofDual {α : Type u_1} [LT α] {a : αᵒᵈ} {b : αᵒᵈ} :
      OrderDual.ofDual a < OrderDual.ofDual b b < a
      theorem OrderDual.le_toDual {α : Type u_1} [LE α] {a : αᵒᵈ} {b : α} :
      a OrderDual.toDual b b OrderDual.ofDual a
      theorem OrderDual.lt_toDual {α : Type u_1} [LT α] {a : αᵒᵈ} {b : α} :
      a < OrderDual.toDual b b < OrderDual.ofDual a
      theorem OrderDual.toDual_le {α : Type u_1} [LE α] {a : α} {b : αᵒᵈ} :
      OrderDual.toDual a b OrderDual.ofDual b a
      theorem OrderDual.toDual_lt {α : Type u_1} [LT α] {a : α} {b : αᵒᵈ} :
      OrderDual.toDual a < b OrderDual.ofDual b < a
      def OrderDual.rec {α : Type u_1} {C : αᵒᵈSort u_2} (h₂ : (a : α) → C (OrderDual.toDual a)) (a : αᵒᵈ) :
      C a

      Recursor for αᵒᵈ.

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

        Alias of the reverse direction of OrderDual.toDual_le_toDual.

        theorem LT.lt.dual {α : Type u_1} [LT α] {a : α} {b : α} :
        b < aOrderDual.toDual a < OrderDual.toDual b

        Alias of the reverse direction of OrderDual.toDual_lt_toDual.

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

        Alias of the reverse direction of OrderDual.ofDual_le_ofDual.

        theorem LT.lt.ofDual {α : Type u_1} [LT α] {a : αᵒᵈ} {b : αᵒᵈ} :
        b < aOrderDual.ofDual a < OrderDual.ofDual 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} :
              toLex.symm = ofLex
              @[simp]
              theorem ofLex_symm_eq {α : Type u_1} :
              ofLex.symm = toLex
              @[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 : Lex α} {b : Lex α} :
              ofLex a = ofLex b a = b
              instance instBEqLex (α : Type u_2) [BEq α] :
              BEq (Lex α)
              Equations
              instance instLawfulBEqLex (α : Type u_2) [BEq α] [LawfulBEq α] :
              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)