Type synonyms

This file provides three 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.
• Colex α: Type synonym of α to equip it with its colexicographic order. The precise meaning depends on the type we take the colex of. Examples include 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 α → α.
• Colex: toColex : α → Colex α and ofColex : Colex α → α.

See also

This file is similar to Algebra.Group.TypeTags.

Order dual

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

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} : toDual.symm = ofDual

@[simp]

theorem OrderDual.ofDual_symm_eq {α : Type u_1} : ofDual.symm = toDual

@[simp]

theorem OrderDual.toDual_ofDual {α : Type u_1} (a : αᵒᵈ) : toDual (ofDual a) = a

@[simp]

theorem OrderDual.ofDual_toDual {α : Type u_1} (a : α) : ofDual (toDual a) = 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

theorem OrderDual.ext {α : Type u_1} {a b : αᵒᵈ} (h : ofDual a = ofDual b) : a = b

theorem OrderDual.ext_iff {α : Type u_1} {a b : αᵒᵈ} : a = b ↔ ofDual a = ofDual b

@[simp]

theorem OrderDual.toDual_le_toDual {α : Type u_1} [LE α] {a b : α} : toDual a ≤ toDual b ↔ b ≤ a

@[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 : αᵒᵈ} : ofDual a ≤ ofDual b ↔ b ≤ a

@[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 : α} : a ≤ toDual b ↔ b ≤ ofDual a

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 : αᵒᵈ} : toDual a ≤ b ↔ ofDual b ≤ a

theorem OrderDual.toDual_lt {α : Type u_1} [LT α] {a : α} {b : αᵒᵈ} : toDual a < b ↔ ofDual b < a

def OrderDual.rec {α : Type u_1} {motive : αᵒᵈ → Sort u_2} (toDual : (a : α) → motive (toDual a)) (a : αᵒᵈ) : motive a

Recursor for αᵒᵈ.

Equations

• OrderDual.rec toDual = toDual

@[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 : α} : 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 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 α)

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)

Colexicographic order

def Colex (α : Type u_2) : Type u_2

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

Equations

• Colex α = α

@[match_pattern]

def toColex {α : Type u_1} : α ≃ Colex α

toColex is the identity function to the Colex of a type.

Equations

• toColex = Equiv.refl α

@[match_pattern]

def ofColex {α : Type u_1} : Colex α ≃ α

ofColex is the identity function from the Colex of a type.

Equations

• ofColex = Equiv.refl (Colex α)

@[simp]

theorem toColex_symm_eq {α : Type u_1} : toColex.symm = ofColex

@[simp]

theorem ofColex_symm_eq {α : Type u_1} : ofColex.symm = toColex

@[simp]

theorem toColex_ofColex {α : Type u_1} (a : Colex α) : toColex (ofColex a) = a

@[simp]

theorem ofColex_toColex {α : Type u_1} (a : α) : ofColex (toColex a) = a

theorem toColex_inj {α : Type u_1} {a b : α} : toColex a = toColex b ↔ a = b

theorem ofColex_inj {α : Type u_1} {a b : Colex α} : ofColex a = ofColex b ↔ a = b

instance instBEqColex (α : Type u_2) [BEq α] : BEq (Colex α)

Equations

• instBEqColex α = { beq := fun (a b : Colex α) => ofColex a == ofColex b }

instance instLawfulBEqColex (α : Type u_2) [BEq α] [LawfulBEq α] : LawfulBEq (Colex α)

instance instDecidableEqColex (α : Type u_2) [DecidableEq α] : DecidableEq (Colex α)

Equations

• instDecidableEqColex α = inferInstanceAs (DecidableEq α)

instance instInhabitedColex (α : Type u_2) [Inhabited α] : Inhabited (Colex α)

Equations

• instInhabitedColex α = inferInstanceAs (Inhabited α)

def Colex.rec {α : Type u_1} {β : Colex α → Sort u_2} (h : (a : α) → β (toColex a)) (a : Colex α) : β a

A recursor for Colex. Use as induction x.

Equations

• Colex.rec h a = h (ofColex a)

@[simp]

theorem Colex.forall {α : Type u_1} {p : Colex α → Prop} : (∀ (a : Colex α), p a) ↔ ∀ (a : α), p (toColex a)

@[simp]

theorem Colex.exists {α : Type u_1} {p : Colex α → Prop} : (∃ (a : Colex α), p a) ↔ ∃ (a : α), p (toColex a)