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≤ b becomes b ≤ a≤ 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 α→ Lex α and ofLex : Lex α → α→ α.

See also #

This file is similar to Algebra.Group.TypeTags.

Order dual #

instance OrderDual.instNontrivialOrderDual {α : Type u_1} [h : Nontrivial α] :

Nontrivial αᵒᵈ

Equations

@OrderDual.instNontrivialOrderDual = @OrderDual.instNontrivialOrderDual.proof_1

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} :

Equiv.symm OrderDual.toDual = OrderDual.ofDual

@[simp]

theorem OrderDual.ofDual_symm_eq {α : Type u_1} :

Equiv.symm OrderDual.ofDual = 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} [inst : LE α] {a : α} {b : α} :

↑OrderDual.toDual a ≤ ↑OrderDual.toDual b ↔ b ≤ a

@[simp]

theorem OrderDual.toDual_lt_toDual {α : Type u_1} [inst : LT α] {a : α} {b : α} :

↑OrderDual.toDual a < ↑OrderDual.toDual b ↔ b < a

@[simp]

theorem OrderDual.ofDual_le_ofDual {α : Type u_1} [inst : LE α] {a : αᵒᵈ} {b : αᵒᵈ} :

↑OrderDual.ofDual a ≤ ↑OrderDual.ofDual b ↔ b ≤ a

@[simp]

theorem OrderDual.ofDual_lt_ofDual {α : Type u_1} [inst : LT α] {a : αᵒᵈ} {b : αᵒᵈ} :

↑OrderDual.ofDual a < ↑OrderDual.ofDual b ↔ b < a

theorem OrderDual.le_toDual {α : Type u_1} [inst : LE α] {a : αᵒᵈ} {b : α} :

a ≤ ↑OrderDual.toDual b ↔ b ≤ ↑OrderDual.ofDual a

theorem OrderDual.lt_toDual {α : Type u_1} [inst : LT α] {a : αᵒᵈ} {b : α} :

a < ↑OrderDual.toDual b ↔ b < ↑OrderDual.ofDual a

theorem OrderDual.toDual_le {α : Type u_1} [inst : LE α] {a : α} {b : αᵒᵈ} :

↑OrderDual.toDual a ≤ b ↔ ↑OrderDual.ofDual b ≤ a

theorem OrderDual.toDual_lt {α : Type u_1} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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_1) :

Type u_1

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} :

Equiv.symm toLex = ofLex

@[simp]

theorem ofLex_symm_eq {α : Type u_1} :

Equiv.symm ofLex = 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

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 using Lex.rec.

Equations

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