doc-next-gen

Mathlib.Order.Synonym

Module docstring

{"# 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 ","### Lexicographic order "}

OrderDual.instNontrivial instance
[h : Nontrivial α] : Nontrivial αᵒᵈ
Full source 
instance [h : Nontrivial α] : Nontrivial αᵒᵈ :=
  h
Nontriviality of Order Duals
Informal description
For any nontrivial type $\alpha$ equipped with an order, the order dual $\alpha^{\text{op}}$ is also nontrivial.
OrderDual.toDual definition
: α ≃ αᵒᵈ
Full source 
/-- `toDual` is the identity function to the `OrderDual` of a linear order. -/
def toDual : α ≃ αᵒᵈ :=
  Equiv.refl _
Identity map to order dual
Informal description
The function maps an element of a linearly ordered type $\alpha$ to its corresponding element in the order dual $\alpha^{\text{op}}$, which is the identity function but interpreted in the dual order where $\leq$ becomes $\geq$ and $<$ becomes $>$.
OrderDual.ofDual definition
: αᵒᵈ ≃ α
Full source 
/-- `ofDual` is the identity function from the `OrderDual` of a linear order. -/
def ofDual : αᵒᵈαᵒᵈ ≃ α :=
  Equiv.refl _
Identity map from order dual
Informal description
The function maps an element of the order dual $\alpha^{\text{op}}$ back to its corresponding element in the original linearly ordered type $\alpha$. This is the identity function but interpreted as a map from the dual order to the original order.
OrderDual.toDual_symm_eq theorem
: (@toDual α).symm = ofDual
Full source 
@[simp]
theorem toDual_symm_eq : (@toDual α).symm = ofDual := rfl
Inverse of Order Dual Equivalence is Dual Order Equivalence
Informal description
The inverse of the equivalence `toDual : α ≃ αᵒᵈ` is equal to `ofDual : αᵒᵈ ≃ α`.
OrderDual.ofDual_symm_eq theorem
: (@ofDual α).symm = toDual
Full source 
@[simp]
theorem ofDual_symm_eq : (@ofDual α).symm = toDual := rfl
Inverse of Order Dual Equivalence is Order Dualization
Informal description
The inverse of the equivalence `ofDual : αᵒᵈ ≃ α` is equal to the equivalence `toDual : α ≃ αᵒᵈ`. In other words, $(α^{\text{op}} \simeq α)^{-1} = (α \simeq α^{\text{op}})$.
OrderDual.toDual_ofDual theorem
(a : αᵒᵈ) : toDual (ofDual a) = a
Full source 
@[simp]
theorem toDual_ofDual (a : αᵒᵈ) : toDual (ofDual a) = a :=
  rfl
Identity Property of Order Dual Maps: $\text{toDual} \circ \text{ofDual} = \text{id}$
Informal description
For any element $a$ in the order dual $\alpha^{\text{op}}$, applying the map `toDual` after `ofDual` returns $a$ itself, i.e., $\text{toDual}(\text{ofDual}(a)) = a$.
OrderDual.ofDual_toDual theorem
(a : α) : ofDual (toDual a) = a
Full source 
@[simp]
theorem ofDual_toDual (a : α) : ofDual (toDual a) = a :=
  rfl
Inverse Order Dual Conversion Preserves Element Identity
Informal description
For any element $a$ of a type $\alpha$, applying the order dual conversion `toDual` followed by its inverse `ofDual` returns the original element, i.e., $\text{ofDual}(\text{toDual}(a)) = a$.
OrderDual.toDual_inj theorem
{a b : α} : toDual a = toDual b ↔ a = b
Full source 
theorem toDual_inj {a b : α} : toDualtoDual a = toDual b ↔ a = b := by simp
Injectivity of Order Dual Map: $a^{\text{op}} = b^{\text{op}} \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ of a type $\alpha$, the equality $a^{\text{op}} = b^{\text{op}}$ holds in the order dual $\alpha^{\text{op}}$ if and only if $a = b$ in $\alpha$.
OrderDual.ofDual_inj theorem
{a b : αᵒᵈ} : ofDual a = ofDual b ↔ a = b
Full source 
theorem ofDual_inj {a b : αᵒᵈ} : ofDualofDual a = ofDual b ↔ a = b := by simp
Injectivity of the Order Dual Coercion
Informal description
For any elements $a$ and $b$ in the order dual $\alpha^{\text{op}}$, the equality $\text{ofDual}(a) = \text{ofDual}(b)$ holds if and only if $a = b$.
OrderDual.toDual_le_toDual theorem
[LE α] {a b : α} : toDual a ≤ toDual b ↔ b ≤ a
Full source 
@[simp]
theorem toDual_le_toDual [LE α] {a b : α} : toDualtoDual a ≤ toDual b ↔ b ≤ a :=
  Iff.rfl
Order Reversal in Dual: $\text{toDual}(a) \leq \text{toDual}(b) \leftrightarrow b \leq a$
Informal description
For any type $\alpha$ equipped with a preorder $\leq$, and for any elements $a, b \in \alpha$, the inequality $\text{toDual}(a) \leq \text{toDual}(b)$ holds in the order dual $\alpha^{\text{op}}$ if and only if $b \leq a$ holds in $\alpha$.
OrderDual.toDual_lt_toDual theorem
[LT α] {a b : α} : toDual a < toDual b ↔ b < a
Full source 
@[simp]
theorem toDual_lt_toDual [LT α] {a b : α} : toDualtoDual a < toDual b ↔ b < a :=
  Iff.rfl
Inequality Reversal in Order Dual: $\text{toDual}(a) < \text{toDual}(b) \leftrightarrow b < a$
Informal description
For any type $\alpha$ equipped with a strict order relation $<$, and for any elements $a, b \in \alpha$, the inequality $\text{toDual}(a) < \text{toDual}(b)$ holds in the order dual $\alpha^{\text{op}}$ if and only if $b < a$ holds in $\alpha$.
OrderDual.ofDual_le_ofDual theorem
[LE α] {a b : αᵒᵈ} : ofDual a ≤ ofDual b ↔ b ≤ a
Full source 
@[simp]
theorem ofDual_le_ofDual [LE α] {a b : αᵒᵈ} : ofDualofDual a ≤ ofDual b ↔ b ≤ a :=
  Iff.rfl
Inequality Reversal in Order Dual via ofDual
Informal description
For any type $\alpha$ with a preorder $\leq$ and elements $a, b$ in the order dual $\alpha^{\text{op}}$, the inequality $\text{ofDual}(a) \leq \text{ofDual}(b)$ holds in $\alpha$ if and only if $b \leq a$ holds in $\alpha^{\text{op}}$.
OrderDual.ofDual_lt_ofDual theorem
[LT α] {a b : αᵒᵈ} : ofDual a < ofDual b ↔ b < a
Full source 
@[simp]
theorem ofDual_lt_ofDual [LT α] {a b : αᵒᵈ} : ofDualofDual a < ofDual b ↔ b < a :=
  Iff.rfl
Inequality Reversal in Order Dual: $\text{ofDual}(a) < \text{ofDual}(b) \leftrightarrow b < a$
Informal description
For any type $\alpha$ equipped with a strict order relation $<$, and for any elements $a, b$ in the order dual $\alpha^{\text{op}}$, the inequality $\text{ofDual}(a) < \text{ofDual}(b)$ holds if and only if $b < a$ in the original order.
OrderDual.le_toDual theorem
[LE α] {a : αᵒᵈ} {b : α} : a ≤ toDual b ↔ b ≤ ofDual a
Full source 
theorem le_toDual [LE α] {a : αᵒᵈ} {b : α} : a ≤ toDual b ↔ b ≤ ofDual a :=
  Iff.rfl
Order Dual Inequality: $a \leq \text{toDual}(b) \leftrightarrow b \leq \text{ofDual}(a)$
Informal description
For any preordered type $\alpha$ and elements $a \in \alpha^{\text{op}}$ and $b \in \alpha$, the inequality $a \leq \text{toDual}(b)$ holds in $\alpha^{\text{op}}$ if and only if $b \leq \text{ofDual}(a)$ holds in $\alpha$.
OrderDual.lt_toDual theorem
[LT α] {a : αᵒᵈ} {b : α} : a < toDual b ↔ b < ofDual a
Full source 
theorem lt_toDual [LT α] {a : αᵒᵈ} {b : α} : a < toDual b ↔ b < ofDual a :=
  Iff.rfl
Strict Order Reversal in Order Dual: $a < \text{toDual}(b) \leftrightarrow b < \text{ofDual}(a)$
Informal description
For any type $\alpha$ with a strict order relation $<$, and for any elements $a$ in the order dual $\alpha^{\text{op}}$ and $b$ in $\alpha$, the inequality $a < \text{toDual}(b)$ holds in $\alpha^{\text{op}}$ if and only if $b < \text{ofDual}(a)$ holds in $\alpha$.
OrderDual.toDual_le theorem
[LE α] {a : α} {b : αᵒᵈ} : toDual a ≤ b ↔ ofDual b ≤ a
Full source 
theorem toDual_le [LE α] {a : α} {b : αᵒᵈ} : toDualtoDual a ≤ b ↔ ofDual b ≤ a :=
  Iff.rfl
Inequality in Order Dual via toDual and ofDual
Informal description
For any type $\alpha$ with a preorder $\leq$, and for any elements $a \in \alpha$ and $b \in \alpha^{\text{op}}$, the inequality $\text{toDual}(a) \leq b$ holds in $\alpha^{\text{op}}$ if and only if $\text{ofDual}(b) \leq a$ holds in $\alpha$.
OrderDual.toDual_lt theorem
[LT α] {a : α} {b : αᵒᵈ} : toDual a < b ↔ ofDual b < a
Full source 
theorem toDual_lt [LT α] {a : α} {b : αᵒᵈ} : toDualtoDual a < b ↔ ofDual b < a :=
  Iff.rfl
Dual Order Inequality: $\text{toDual}(a) < b \leftrightarrow \text{ofDual}(b) < a$
Informal description
For any type $\alpha$ equipped with a strict order relation $<$, and for any elements $a \in \alpha$ and $b \in \alpha^{\text{op}}$, the inequality $\text{toDual}(a) < b$ holds in the order dual $\alpha^{\text{op}}$ if and only if $\text{ofDual}(b) < a$ holds in the original order $\alpha$.
OrderDual.rec definition
{C : αᵒᵈ → Sort*} (h₂ : ∀ a : α, C (toDual a)) : ∀ a : αᵒᵈ, C a
Full source 
/-- Recursor for `αᵒᵈ`. -/
@[elab_as_elim]
protected def rec {C : αᵒᵈ → Sort*} (h₂ : ∀ a : α, C (toDual a)) : ∀ a : αᵒᵈ, C a :=
  h₂
Recursor for order dual type
Informal description
The recursor for the order dual type `αᵒᵈ` allows defining a dependent function on `αᵒᵈ` by specifying its values on elements of the form `toDual a` for `a : α`. Specifically, given a type family `C : αᵒᵈ → Sort*` and a function `h₂ : ∀ a : α, C (toDual a)`, the recursor produces a function `∀ a : αᵒᵈ, C a`.
OrderDual.forall theorem
{p : αᵒᵈ → Prop} : (∀ a, p a) ↔ ∀ a, p (toDual a)
Full source 
@[simp]
protected theorem «forall» {p : αᵒᵈ → Prop} : (∀ a, p a) ↔ ∀ a, p (toDual a) :=
  Iff.rfl
Universal Quantification in Order Dual
Informal description
For any predicate $p$ on the order dual $\alpha^{\text{op}}$, the universal quantification $\forall a \in \alpha^{\text{op}}, p(a)$ holds if and only if $\forall a \in \alpha, p(\text{toDual}(a))$ holds.
OrderDual.exists theorem
{p : αᵒᵈ → Prop} : (∃ a, p a) ↔ ∃ a, p (toDual a)
Full source 
@[simp]
protected theorem «exists» {p : αᵒᵈ → Prop} : (∃ a, p a) ↔ ∃ a, p (toDual a) :=
  Iff.rfl
Existence in Order Dual is Equivalent to Existence in Original Type
Informal description
For any predicate $p$ on the order dual $\alpha^{\text{op}}$, there exists an element $a$ in $\alpha^{\text{op}}$ satisfying $p(a)$ if and only if there exists an element $a$ in $\alpha$ satisfying $p(\text{toDual}(a))$.
Lex definition
(α : Type*)
Full source 
/-- A type synonym to equip a type with its lexicographic order. -/
def Lex (α : Type*) :=
  α
Lexicographic order type synonym
Informal description
The type synonym `Lex α` equips a type `α` with its lexicographic order. This allows us to treat `α` as having a different ordering structure while maintaining the same underlying type. The conversion between `α` and `Lex α` is done via the explicit coercions `toLex : α → Lex α` and `ofLex : Lex α → α`.
toLex definition
: α ≃ Lex α
Full source 
/-- `toLex` is the identity function to the `Lex` of a type. -/
@[match_pattern]
def toLex : α ≃ Lex α :=
  Equiv.refl _
Canonical equivalence to lexicographic order type
Informal description
The function `toLex` is the identity equivalence between a type `α` and its lexicographic order type synonym `Lex α`. It serves as the canonical bijection that preserves the underlying elements while changing the order structure.
ofLex definition
: Lex α ≃ α
Full source 
/-- `ofLex` is the identity function from the `Lex` of a type. -/
@[match_pattern]
def ofLex : LexLex α ≃ α :=
  Equiv.refl _
Conversion from lexicographic order to original type
Informal description
The function `ofLex` is the identity function that converts an element from the lexicographic order type synonym `Lex α` back to the original type `α`.
toLex_symm_eq theorem
: (@toLex α).symm = ofLex
Full source 
@[simp]
theorem toLex_symm_eq : (@toLex α).symm = ofLex :=
  rfl
Inverse of Lexicographic Order Equivalence Equals Conversion Function
Informal description
The inverse of the canonical equivalence `toLex` from a type `α` to its lexicographic order type synonym `Lex α` is equal to the conversion function `ofLex` from `Lex α` back to `α`.
ofLex_symm_eq theorem
: (@ofLex α).symm = toLex
Full source 
@[simp]
theorem ofLex_symm_eq : (@ofLex α).symm = toLex :=
  rfl
Inverse of Lexicographic Order Conversion Equals Forward Conversion
Informal description
The inverse of the equivalence `ofLex : Lex α ≃ α` is equal to the equivalence `toLex : α ≃ Lex α`.
toLex_ofLex theorem
(a : Lex α) : toLex (ofLex a) = a
Full source 
@[simp]
theorem toLex_ofLex (a : Lex α) : toLex (ofLex a) = a :=
  rfl
$\text{toLex} \circ \text{ofLex} = \text{id}$ on $\text{Lex}(\alpha)$
Informal description
For any element $a$ of the lexicographic order type synonym $\text{Lex}(\alpha)$, the composition of the conversion functions $\text{toLex} \circ \text{ofLex}$ applied to $a$ returns $a$ itself.
ofLex_toLex theorem
(a : α) : ofLex (toLex a) = a
Full source 
@[simp]
theorem ofLex_toLex (a : α) : ofLex (toLex a) = a :=
  rfl
Identity Property of Lexicographic Order Conversions
Informal description
For any element $a$ of type $\alpha$, applying the conversion from lexicographic order `ofLex` to the conversion to lexicographic order `toLex` of $a$ returns $a$ itself, i.e., $\text{ofLex}(\text{toLex}(a)) = a$.
toLex_inj theorem
{a b : α} : toLex a = toLex b ↔ a = b
Full source 
theorem toLex_inj {a b : α} : toLextoLex a = toLex b ↔ a = b := by simp
Injectivity of Lexicographic Order Embedding
Informal description
For any elements $a$ and $b$ of a type $\alpha$, the lexicographic order embeddings satisfy $\text{toLex}(a) = \text{toLex}(b)$ if and only if $a = b$.
ofLex_inj theorem
{a b : Lex α} : ofLex a = ofLex b ↔ a = b
Full source 
theorem ofLex_inj {a b : Lex α} : ofLexofLex a = ofLex b ↔ a = b := by simp
Injectivity of `ofLex` for Lexicographic Order
Informal description
For any two elements $a$ and $b$ of the lexicographic order type `Lex α`, the equality `ofLex a = ofLex b` holds if and only if $a = b$ in `Lex α$.
instBEqLex instance
(α : Type*) [BEq α] : BEq (Lex α)
Full source 
instance (α : Type*) [BEq α] : BEq (Lex α) where
  beq a b := ofLex a == ofLex b
Boolean Equality on Lexicographic Order Type Synonym
Informal description
For any type $\alpha$ equipped with a boolean equality relation, the lexicographic order type synonym $\text{Lex}\,\alpha$ also inherits a boolean equality relation.
instLawfulBEqLex instance
(α : Type*) [BEq α] [LawfulBEq α] : LawfulBEq (Lex α)
Full source 
instance (α : Type*) [BEq α] [LawfulBEq α] : LawfulBEq (Lex α) :=
  inferInstanceAs (LawfulBEq α)
Lawful Boolean Equality for Lexicographic Order Type Synonym
Informal description
For any type $\alpha$ equipped with a boolean equality relation and satisfying the lawful boolean equality properties, the lexicographic order type synonym $\text{Lex}\,\alpha$ also satisfies the lawful boolean equality properties.
instDecidableEqLex instance
(α : Type*) [DecidableEq α] : DecidableEq (Lex α)
Full source 
instance (α : Type*) [DecidableEq α] : DecidableEq (Lex α) :=
  inferInstanceAs (DecidableEq α)
Decidable Equality for Lexicographic Order Type Synonym
Informal description
For any type $\alpha$ with a decidable equality, the lexicographic order type synonym $\text{Lex}\,\alpha$ also has a decidable equality.
instInhabitedLex instance
(α : Type*) [Inhabited α] : Inhabited (Lex α)
Full source 
instance (α : Type*) [Inhabited α] : Inhabited (Lex α) :=
  inferInstanceAs (Inhabited α)
Inhabited Lexicographic Order Type Synonym
Informal description
For any inhabited type $\alpha$, the lexicographic order type synonym $\text{Lex}\,\alpha$ is also inhabited.
Lex.rec definition
{β : Lex α → Sort*} (h : ∀ a, β (toLex a)) : ∀ a, β a
Full source 
/-- A recursor for `Lex`. Use as `induction x`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
protected def Lex.rec {β : Lex α → Sort*} (h : ∀ a, β (toLex a)) : ∀ a, β a := fun a => h (ofLex a)
Recursor for lexicographic order type
Informal description
The recursor for the lexicographic order type synonym `Lex α`. Given a type family `β` indexed by `Lex α` and a function `h` that defines `β (toLex a)` for all `a : α`, this recursor allows defining a function that produces an element of `β a` for any `a : Lex α` by using the canonical equivalence between `α` and `Lex α`.
Lex.forall theorem
{p : Lex α → Prop} : (∀ a, p a) ↔ ∀ a, p (toLex a)
Full source 
@[simp] lemma Lex.forall {p : Lex α → Prop} : (∀ a, p a) ↔ ∀ a, p (toLex a) := Iff.rfl
Universal Quantification over Lexicographic Order Type
Informal description
For any predicate $p$ on the lexicographic order type $\text{Lex}\,\alpha$, the universal quantification $\forall a \in \text{Lex}\,\alpha, p(a)$ holds if and only if $\forall a \in \alpha, p(\text{toLex}\,a)$ holds.
Lex.exists theorem
{p : Lex α → Prop} : (∃ a, p a) ↔ ∃ a, p (toLex a)
Full source 
@[simp] lemma Lex.exists {p : Lex α → Prop} : (∃ a, p a) ↔ ∃ a, p (toLex a) := Iff.rfl
Existence Transfer Between Lexicographic Order and Original Type
Informal description
For any predicate $p$ on the lexicographic order type `Lex α`, there exists an element $a$ in `Lex α` satisfying $p(a)$ if and only if there exists an element $a$ in the original type $α$ such that $p(\text{toLex}(a))$ holds, where $\text{toLex} : α → \text{Lex} α$ is the canonical embedding.