Type synonyms

This file provides two type synonyms for order theory:

• 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, DFinsupp, Finsupp.

Notation

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:

• Lex: toLex : α → Lex α and ofLex : Lex α → α.
• Colex: toColex : α → Colex α and ofColex : Colex α → α.

See also

This file is similar to Mathlib.Algebra.Group.TypeTags.Basic.

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

@[implicit_reducible]

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 α] [h : LawfulBEq α] : LawfulBEq (Lex α)

@[implicit_reducible]

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

Equations

• instDecidableEqLex α = h

@[implicit_reducible]

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

Equations

• instInhabitedLex α = h

instance instNonemptyLex (α : Type u_2) [h : Nonempty α] : Nonempty (Lex α)

instance instNontrivialLex (α : Type u_2) [h : Nontrivial α] : Nontrivial (Lex α)

@[implicit_reducible]

instance instUniqueLex (α : Type u_2) [h : Unique α] : Unique (Lex α)

Equations

• instUniqueLex α = h

@[implicit_reducible]

instance instCoeFunLex {α : Type u_2} {γ : α → Sort u_3} [H : CoeFun α γ] : CoeFun (Lex α) γ

Equations

• instCoeFunLex = { coe := fun (f : Lex α) => CoeFun.coe (ofLex f) }

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

@[implicit_reducible]

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 α] [h : LawfulBEq α] : LawfulBEq (Colex α)

@[implicit_reducible]

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

Equations

• instDecidableEqColex α = h

@[implicit_reducible]

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

Equations

• instInhabitedColex α = h

instance instNonemptyColex (α : Type u_2) [h : Nonempty α] : Nonempty (Colex α)

instance instNontrivialColex (α : Type u_2) [h : Nontrivial α] : Nontrivial (Colex α)

@[implicit_reducible]

instance instUniqueColex (α : Type u_2) [h : Unique α] : Unique (Colex α)

Equations

• instUniqueColex α = h

@[implicit_reducible]

instance instCoeFunColex {α : Type u_2} {γ : α → Sort u_3} [H : CoeFun α γ] : CoeFun (Colex α) γ

Equations

• instCoeFunColex = { coe := fun (f : Colex α) => CoeFun.coe (ofColex f) }

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)