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.instNontrivial {α : Type u_1} [h : Nontrivial α] : Nontrivial αᵒᵈ

Equations

• ⋯ = h

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

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

Equations

• OrderDual.toDual = Equiv.refl α

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

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

Equations

• OrderDual.ofDual = Equiv.refl αᵒᵈ

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

• OrderDual.rec h₂ = h₂

@[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_2) : Type u_2

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

Equations

• Lex α = α

@[match_pattern]

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

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

Equations

• toLex = Equiv.refl α

@[match_pattern]

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

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

Equations

• ofLex = Equiv.refl (Lex α)

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

• instBEqLex α = { beq := fun (a b : Lex α) => ofLex a == ofLex b }

instance instLawfulBEqLex (α : Type u_2) [BEq α] [LawfulBEq α] : LawfulBEq (Lex α)

Equations

• ⋯ = ⋯

instance instDecidableEqLex (α : Type u_2) [DecidableEq α] : DecidableEq (Lex α)

Equations

• instDecidableEqLex α = inferInstanceAs (DecidableEq α)

instance instInhabitedLex (α : Type u_2) [Inhabited α] : Inhabited (Lex α)

Equations

• instInhabitedLex α = inferInstanceAs (Inhabited α)

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

• Lex.rec h a = h (ofLex a)

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