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.instNontrivialOrderDual {α : Type u_1} [h : Nontrivial α] :

Nontrivial αᵒᵈ

Equations

⋯ = h

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

OrderDual.toDual.symm = OrderDual.ofDual

@[simp]

theorem OrderDual.ofDual_symm_eq {α : Type u_1} :

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

def OrderDual.rec {α : Type u_1} {C : αᵒᵈ → Sort u_4} (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} [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_4) :

Type u_4

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

ofLex a = ofLex b ↔ a = b

def Lex.rec {α : Type u_1} {β : Lex α → Sort u_4} (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)

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