mathlib3 documentation

order.synonym

Type synonyms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides two type synonyms for order theory:

Notation #

αᵒᵈ is notation for order_dual α.

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:

In fact, those are bundled as equivs to put goals in the right syntactic form for rewriting with the equiv API (⇑to_lex a where ⇑ is coe_fn : (α ≃ lex α) → α → lex α, instead of a bare to_lex a).

See also #

This file is similar to algebra.group.type_tags.

Order dual #

source
@[protected, instance]
def order_dual.nontrivial {α : Type u_1} [h : nontrivial α] :
nontrivial αᵒᵈ
source
def order_dual.to_dual {α : Type u_1} :
α ≃ αᵒᵈ

to_dual is the identity function to the order_dual of a linear order.

Equations
source
def order_dual.of_dual {α : Type u_1} :
αᵒᵈ ≃ α

of_dual is the identity function from the order_dual of a linear order.

Equations
source
@[simp]
theorem order_dual.to_dual_symm_eq {α : Type u_1} :
order_dual.to_dual.symm = order_dual.of_dual
source
@[simp]
theorem order_dual.of_dual_symm_eq {α : Type u_1} :
order_dual.of_dual.symm = order_dual.to_dual
source
@[simp]
theorem order_dual.to_dual_of_dual {α : Type u_1} (a : αᵒᵈ) :
⇑order_dual.to_dual (⇑order_dual.of_dual a) = a
source
@[simp]
theorem order_dual.of_dual_to_dual {α : Type u_1} (a : α) :
⇑order_dual.of_dual (⇑order_dual.to_dual a) = a
source
@[simp]
theorem order_dual.to_dual_inj {α : Type u_1} {a b : α} :
⇑order_dual.to_dual a = ⇑order_dual.to_dual b ↔ a = b
source
@[simp]
theorem order_dual.of_dual_inj {α : Type u_1} {a b : αᵒᵈ} :
⇑order_dual.of_dual a = ⇑order_dual.of_dual b ↔ a = b
source
@[simp]
theorem order_dual.to_dual_le_to_dual {α : Type u_1} [has_le α] {a b : α} :
⇑order_dual.to_dual a ≤ ⇑order_dual.to_dual b ↔ b ≤ a
source
@[simp]
theorem order_dual.to_dual_lt_to_dual {α : Type u_1} [has_lt α] {a b : α} :
⇑order_dual.to_dual a < ⇑order_dual.to_dual b ↔ b < a
source
@[simp]
theorem order_dual.of_dual_le_of_dual {α : Type u_1} [has_le α] {a b : αᵒᵈ} :
⇑order_dual.of_dual a ≤ ⇑order_dual.of_dual b ↔ b ≤ a
source
@[simp]
theorem order_dual.of_dual_lt_of_dual {α : Type u_1} [has_lt α] {a b : αᵒᵈ} :
⇑order_dual.of_dual a < ⇑order_dual.of_dual b ↔ b < a
source
theorem order_dual.le_to_dual {α : Type u_1} [has_le α] {a : αᵒᵈ} {b : α} :
a ≤ ⇑order_dual.to_dual b ↔ b ≤ ⇑order_dual.of_dual a
source
theorem order_dual.lt_to_dual {α : Type u_1} [has_lt α] {a : αᵒᵈ} {b : α} :
a < ⇑order_dual.to_dual b ↔ b < ⇑order_dual.of_dual a
source
theorem order_dual.to_dual_le {α : Type u_1} [has_le α] {a : α} {b : αᵒᵈ} :
⇑order_dual.to_dual a ≤ b ↔ ⇑order_dual.of_dual b ≤ a
source
theorem order_dual.to_dual_lt {α : Type u_1} [has_lt α] {a : α} {b : αᵒᵈ} :
⇑order_dual.to_dual a < b ↔ ⇑order_dual.of_dual b < a
source
@[protected]
def order_dual.rec {α : Type u_1} {C : αᵒᵈ → Sort u_2} (h₂ : Π (a : α), C (⇑order_dual.to_dual a)) (a : αᵒᵈ) :
C a

Recursor for αᵒᵈ.

Equations
source
@[protected, simp]
theorem order_dual.forall {α : Type u_1} {p : αᵒᵈ → Prop} :
(∀ (a : αᵒᵈ), p a) ↔ ∀ (a : α), p (⇑order_dual.to_dual a)
source
@[protected, simp]
theorem order_dual.exists {α : Type u_1} {p : αᵒᵈ → Prop} :
(∃ (a : αᵒᵈ), p a) ↔ ∃ (a : α), p (⇑order_dual.to_dual a)
source
theorem has_le.le.dual {α : Type u_1} [has_le α] {a b : α} :
b ≤ a → ⇑order_dual.to_dual a ≤ ⇑order_dual.to_dual b

Alias of the reverse direction of order_dual.to_dual_le_to_dual.

source
theorem has_lt.lt.dual {α : Type u_1} [has_lt α] {a b : α} :
b < a → ⇑order_dual.to_dual a < ⇑order_dual.to_dual b

Alias of the reverse direction of order_dual.to_dual_lt_to_dual.

source
theorem has_le.le.of_dual {α : Type u_1} [has_le α] {a b : αᵒᵈ} :
b ≤ a → ⇑order_dual.of_dual a ≤ ⇑order_dual.of_dual b

Alias of the reverse direction of order_dual.of_dual_le_of_dual.

source
theorem has_lt.lt.of_dual {α : Type u_1} [has_lt α] {a b : αᵒᵈ} :
b < a → ⇑order_dual.of_dual a < ⇑order_dual.of_dual b

Alias of the reverse direction of order_dual.of_dual_lt_of_dual.

Lexicographic order #

source
def lex (α : Type u_1) :
Type u_1

A type synonym to equip a type with its lexicographic order.

Equations
Instances for lex
source
def to_lex {α : Type u_1} :
α ≃ lex α

to_lex is the identity function to the lex of a type.

Equations
source
def of_lex {α : Type u_1} :
lex α ≃ α

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

Equations
source
@[simp]
theorem to_lex_symm_eq {α : Type u_1} :
to_lex.symm = of_lex
source
@[simp]
theorem of_lex_symm_eq {α : Type u_1} :
of_lex.symm = to_lex
source
@[simp]
theorem to_lex_of_lex {α : Type u_1} (a : lex α) :
⇑to_lex (⇑of_lex a) = a
source
@[simp]
theorem of_lex_to_lex {α : Type u_1} (a : α) :
⇑of_lex (⇑to_lex a) = a
source
@[simp]
theorem to_lex_inj {α : Type u_1} {a b : α} :
⇑to_lex a = ⇑to_lex b ↔ a = b
source
@[simp]
theorem of_lex_inj {α : Type u_1} {a b : lex α} :
⇑of_lex a = ⇑of_lex b ↔ a = b
source
@[protected]
def lex.rec {α : Type u_1} {β : lex α → Sort u_2} (h : Π (a : α), β (⇑to_lex a)) (a : lex α) :
β a

A recursor for lex. Use as induction x using lex.rec.

Equations