Documentation

Mathlib.Order.Synonym

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 αᵒᵈ

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

@[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} {C : αᵒᵈ → Sort u_2} (h₂ : (a : α) → C (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 (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 α = α

Instances For

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