# 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 α → α.

This file is similar to Algebra.Group.TypeTags.

### Order dual #

instance OrderDual.instNontrivialOrderDual {α : Type u_1} [h : ] :
def OrderDual.toDual {α : Type u_1} :
α αᵒᵈ

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

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

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

Instances For
@[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 αᵒᵈ.

Instances For
@[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 aOrderDual.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 < aOrderDual.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 aOrderDual.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 < aOrderDual.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.

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

Instances For