Documentation

Mathlib.Order.Synonym

Type synonyms #

This file provides two type synonyms for order theory:

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:

See also #

This file is similar to Algebra.Group.TypeTags.

Order dual #

def OrderDual.toDual {α : Type u_1} :
α αᵒᵈ

toDual is the identity function to the OrderDual of a linear order.

Equations
def OrderDual.ofDual {α : Type u_1} :
αᵒᵈ α

ofDual is the identity function from the OrderDual of a linear order.

Equations
@[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
@[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 aOrderDual.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 < aOrderDual.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 aOrderDual.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 < aOrderDual.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
@[match_pattern]
def toLex {α : Type u_1} :
α Lex α

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

Equations
@[match_pattern]
def ofLex {α : Type u_1} :
Lex α α

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

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