Type synonyms

This file provides two type synonyms for order theory:

• OrderDual α: Type synonym of α to equip it with the dual order (a ≤ b becomes b ≤ a).
• Lex α: Type synonym of α to equip it with its lexicographic order. The precise meaning depends on the type we take the lex of. Examples include Prod, Sigma, List, Finset.

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:

• OrderDual: OrderDual.toDual : α → αᵒᵈ and OrderDual.ofDual : αᵒᵈ → α
• Lex: toLex : α → Lex α and ofLex : Lex α → α.

See also

This file is similar to Algebra.Group.TypeTags.

Order dual

instance OrderDual.instNontrivialOrderDual {α : Type u_1} [h : Nontrivial α] : Nontrivial αᵒᵈ

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

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

def OrderDual.ofDual {α : Type u_1} : αᵒᵈ ≃ α

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

@[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_4} (h₂ : (a : α) → C (↑OrderDual.toDual a)) (a : αᵒᵈ) : C a

Recursor 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 ≤ a → ↑OrderDual.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 < a → ↑OrderDual.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 ≤ a → ↑OrderDual.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 < a → ↑OrderDual.ofDual a < ↑OrderDual.ofDual b

Alias of the reverse direction of OrderDual.ofDual_lt_ofDual.

Lexicographic order

def Lex (α : Type u_4) : Type u_4

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

@[match_pattern]

def toLex {α : Type u_1} : α ≃ Lex α

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

@[match_pattern]

def ofLex {α : Type u_1} : Lex α ≃ α

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

@[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

def Lex.rec {α : Type u_1} {β : Lex α → Sort u_4} (h : (a : α) → β (↑toLex a)) (a : Lex α) : β a

A recursor for Lex. Use as induction x using Lex.rec.