Documentation

Mathlib.Order.Lex

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.

Instances For

@[match_pattern]

def toLex {α : Type u_1} :

α ≃ Lex α

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

Instances For

@[match_pattern]

def ofLex {α : Type u_1} :

Lex α ≃ α

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

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 b : Lex α} :

ofLex a = ofLex b ↔ a = b

@[implicit_reducible]

instance instBEqLex (α : Type u_2) [BEq α] :

BEq (Lex α)

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

LawfulBEq (Lex α)

@[implicit_reducible]

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

DecidableEq (Lex α)

@[implicit_reducible]

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

Inhabited (Lex α)

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 α)

@[implicit_reducible]

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

CoeFun (Lex α) γ

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.

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)

Colexicographic order #

def Colex (α : Type u_2) :

Type u_2

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

Instances For

@[match_pattern]

def toColex {α : Type u_1} :

α ≃ Colex α

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

Instances For

@[match_pattern]

def ofColex {α : Type u_1} :

Colex α ≃ α

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

Instances For

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

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

LawfulBEq (Colex α)

@[implicit_reducible]

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

DecidableEq (Colex α)

@[implicit_reducible]

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

Inhabited (Colex α)

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 α)

@[implicit_reducible]

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

CoeFun (Colex α) γ

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.

Instances For

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