Mathlib.Data.Prod.Lex

Prod.Lex.term_×ₗ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] notation:35 α " ×ₗ " β:34 => Lex (Prod α β)

Lexicographic product order notation

Informal description

The notation `α ×ₗ β` represents the lexicographic order on the product type `α × β`, where `α` and `β` are ordered types. This means that for pairs `(a₁, b₁)` and `(a₂, b₂)` in `α × β`, we have `(a₁, b₁) ≤ (a₂, b₂)` in the lexicographic order if either `a₁ < a₂` in `α`, or `a₁ = a₂` and `b₁ ≤ b₂` in `β`.

Prod.Lex.instLE instance

(α β : Type*) [LT α] [LE β] : LE (α ×ₗ β)

Full source

/-- Dictionary / lexicographic ordering on pairs. -/
instance instLE (α β : Type*) [LT α] [LE β] : LE (α ×ₗ β) where le := Prod.Lex (· < ·) (· ≤ ·)

Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with a strict order $<$ on $\alpha$ and a non-strict order $\leq$ on $\beta$, the lexicographic product $\alpha \times_\ell \beta$ is equipped with a non-strict order $\leq$ defined by $(a_1, b_1) \leq (a_2, b_2)$ if and only if either $a_1 < a_2$ or ($a_1 = a_2$ and $b_1 \leq b_2$).

Prod.Lex.instLT instance

(α β : Type*) [LT α] [LT β] : LT (α ×ₗ β)

Full source

instance instLT (α β : Type*) [LT α] [LT β] : LT (α ×ₗ β) where lt := Prod.Lex (· < ·) (· < ·)

Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with strict orders $<$ on $\alpha$ and $\beta$, the lexicographic product $\alpha \times_\ell \beta$ is also equipped with a strict order $<$, where $(a_1, b_1) < (a_2, b_2)$ if and only if either $a_1 < a_2$ or $a_1 = a_2$ and $b_1 < b_2$.

Prod.Lex.toLex_le_toLex theorem

[LT α] [LE β] {x y : α × β} : toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2

Full source

theorem toLex_le_toLex [LT α] [LE β] {x y : α × β} :
    toLextoLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 :=
  Prod.lex_def

Lexicographic Order Characterization for Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with a strict order $<$ on $\alpha$ and a non-strict order $\leq$ on $\beta$, and for any pairs $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in $\alpha \times \beta$, the lexicographic order satisfies: $$ \text{toLex}(x) \leq \text{toLex}(y) \iff x_1 < y_1 \lor (x_1 = y_1 \land x_2 \leq y_2). $$

Prod.Lex.toLex_lt_toLex theorem

[LT α] [LT β] {x y : α × β} : toLex x < toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2

Full source

theorem toLex_lt_toLex [LT α] [LT β] {x y : α × β} :
    toLextoLex x < toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 :=
  Prod.lex_def

Characterization of Strict Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with strict orders $<$, and for any pairs $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in $\alpha \times \beta$, the lexicographic order satisfies: $$\text{toLex}(x) < \text{toLex}(y) \iff x_1 < y_1 \lor (x_1 = y_1 \land x_2 < y_2).$$

Prod.Lex.le_iff theorem

 [LT α] [LE β] {x y : α ×ₗ β} :
  x ≤ y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 ≤ (ofLex y).2

Full source

lemma le_iff [LT α] [LE β] {x y : α ×ₗ β} :
    x ≤ y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 ≤ (ofLex y).2 :=
  Prod.lex_def

Characterization of Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with a strict order $<$ on $\alpha$ and a non-strict order $\leq$ on $\beta$, and for any elements $x, y$ in the lexicographic product $\alpha \times_\ell \beta$, we have $x \leq y$ if and only if either the first component of $x$ is strictly less than the first component of $y$, or the first components are equal and the second component of $x$ is less than or equal to the second component of $y$. In symbols: $$ x \leq y \iff \text{ofLex}(x)_1 < \text{ofLex}(y)_1 \lor \left(\text{ofLex}(x)_1 = \text{ofLex}(y)_1 \land \text{ofLex}(x)_2 \leq \text{ofLex}(y)_2\right) $$

Prod.Lex.lt_iff theorem

 [LT α] [LT β] {x y : α ×ₗ β} :
  x < y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 < (ofLex y).2

Full source

lemma lt_iff [LT α] [LT β] {x y : α ×ₗ β} :
    x < y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 < (ofLex y).2 :=
  Prod.lex_def

Characterization of Strict Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with strict orders $<$, and for any elements $x, y$ in the lexicographic product $\alpha \times_\ell \beta$, we have $x < y$ if and only if either the first component of $x$ is strictly less than the first component of $y$, or the first components are equal and the second component of $x$ is strictly less than the second component of $y$. In symbols: $$ x < y \iff \text{ofLex}(x)_1 < \text{ofLex}(y)_1 \lor \left(\text{ofLex}(x)_1 = \text{ofLex}(y)_1 \land \text{ofLex}(x)_2 < \text{ofLex}(y)_2\right) $$

Prod.Lex.instWellFoundedLTLex instance

[LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedLT (α ×ₗ β)

Full source

instance [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedLT (α ×ₗ β) :=
  instIsWellFounded

Well-foundedness of Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with strict orders $<$ and well-founded strict orders on $\alpha$ and $\beta$, the lexicographic product $\alpha \times_\ell \beta$ also has a well-founded strict order.

Prod.Lex.instWellFoundedRelationLexOfWellFoundedLT instance

[LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedRelation (α ×ₗ β)

Full source

instance [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedRelation (α ×ₗ β) :=
  ⟨(· < ·), wellFounded_lt⟩

Well-foundedness of Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ with well-founded strict orders $<$, the lexicographic product $\alpha \times_\ell \beta$ is also well-founded with respect to the lexicographic order.

Prod.Lex.instPreorder instance

(α β : Type*) [Preorder α] [Preorder β] : Preorder (α ×ₗ β)

Full source

/-- Dictionary / lexicographic preorder for pairs. -/
instance instPreorder (α β : Type*) [Preorder α] [Preorder β] : Preorder (α ×ₗ β) where
  le_refl := refl_of <| Prod.Lex _ _
  le_trans _ _ _ := trans_of <| Prod.Lex _ _
  lt_iff_le_not_le x₁ x₂ := by aesop (add simp [le_iff, lt_iff, lt_iff_le_not_le])

Lexicographic Preorder on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with preorders, the lexicographic product $\alpha \times_\ell \beta$ is also equipped with a preorder. The order relation is defined by $(a_1, b_1) \leq (a_2, b_2)$ if and only if either $a_1 < a_2$ or ($a_1 = a_2$ and $b_1 \leq b_2$).

Prod.Lex.monotone_fst theorem

[Preorder α] [LE β] (t c : α ×ₗ β) (h : t ≤ c) : (ofLex t).1 ≤ (ofLex c).1

Full source

/-- See also `monotone_fst_ofLex` for a version stated in terms of `Monotone`. -/
theorem monotone_fst [Preorder α] [LE β] (t c : α ×ₗ β) (h : t ≤ c) :
    (ofLex t).1 ≤ (ofLex c).1 := by
  cases toLex_le_toLex.mp h with
  | inl h' => exact h'.le
  | inr h' => exact h'.1.le

Monotonicity of the First Projection under Lexicographic Order

Informal description

Let $\alpha$ be a preorder and $\beta$ be a type equipped with a non-strict order $\leq$. For any two elements $t$ and $c$ in the lexicographic product $\alpha \times_\ell \beta$, if $t \leq c$ in the lexicographic order, then the first component of $t$ is less than or equal to the first component of $c$ in the preorder on $\alpha$.

Prod.Lex.monotone_fst_ofLex theorem

: Monotone fun x : α ×ₗ β ↦ (ofLex x).1

Full source

theorem monotone_fst_ofLex : Monotone fun x : α ×ₗ β ↦ (ofLex x).1 := monotone_fst

Monotonicity of the First Projection in Lexicographic Order

Informal description

The first projection function from the lexicographic product $\alpha \times_\ell \beta$ to $\alpha$ is monotone. That is, for any $x, y \in \alpha \times_\ell \beta$, if $x \leq y$ in the lexicographic order, then $(x).1 \leq (y).1$ in the preorder on $\alpha$.

Prod.Lex.toLex_covBy_toLex_iff theorem

 {a₁ a₂ : α} {b₁ b₂ : β} : toLex (a₁, b₁) ⋖ toLex (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ ⋖ b₂ ∨ a₁ ⋖ a₂ ∧ IsMax b₁ ∧ IsMin b₂

Full source

theorem toLex_covBy_toLex_iff {a₁ a₂ : α} {b₁ b₂ : β} :
    toLextoLex (a₁, b₁) ⋖ toLex (a₂, b₂)toLex (a₁, b₁) ⋖ toLex (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ ⋖ b₂ ∨ a₁ ⋖ a₂ ∧ IsMax b₁ ∧ IsMin b₂ := by
  simp only [CovBy, toLex_lt_toLex, toLex.surjective.forall, Prod.forall, isMax_iff_forall_not_lt,
    isMin_iff_forall_not_lt]
  constructor
  · rintro ⟨ha | ⟨rfl, hb⟩, h₂⟩
    · refine .inr ⟨⟨ha, fun c hc₁ hc₂ ↦ ?_⟩, fun c hc ↦ ?_, fun c hc ↦ ?_⟩
      · exact h₂ c b₁ (.inl hc₁) (.inl hc₂)
      · exact h₂ a₁ c (.inr ⟨rfl, hc⟩) (.inl ha)
      · exact h₂ a₂ c (.inl ha) (.inr ⟨rfl, hc⟩)
    · exact .inl ⟨rfl, hb, fun c hc₁ hc₂ ↦ h₂ _ _ (.inr ⟨rfl, hc₁⟩) (.inr ⟨rfl, hc₂⟩)⟩
  · rintro (⟨rfl, hb, h⟩ | ⟨⟨ha, h⟩, hb₁, hb₂⟩)
    · refine ⟨.inr ⟨rfl, hb⟩, fun a b ↦ ?_⟩
      rintro (hlt₁ | ⟨rfl, hlt₁⟩) (hlt₂ | ⟨heq, hlt₂⟩)
      exacts [hlt₁.not_lt hlt₂, hlt₁.ne' heq, hlt₂.false, h hlt₁ hlt₂]
    · refine ⟨.inl ha, fun a b ↦ ?_⟩
      rintro (hlt₁ | ⟨rfl, hlt₁⟩) (hlt₂ | ⟨heq, hlt₂⟩)
      exacts [h hlt₁ hlt₂, hb₂ _ hlt₂, hb₁ _ hlt₁, hb₁ _ hlt₁]

Covering Relation in Lexicographic Order: $(a_1, b_1) \lessdot (a_2, b_2)$ iff $a_1 = a_2 \land b_1 \lessdot b_2$ or $a_1 \lessdot a_2 \land b_1$ maximal $\land b_2$ minimal

Informal description

Let $\alpha$ and $\beta$ be types with strict orders, and let $(a_1, b_1), (a_2, b_2) \in \alpha \times \beta$. The lexicographic order satisfies $(a_1, b_1) \lessdot (a_2, b_2)$ if and only if either: 1. $a_1 = a_2$ and $b_1 \lessdot b_2$ in $\beta$, or 2. $a_1 \lessdot a_2$ in $\alpha$, $b_1$ is maximal in $\beta$, and $b_2$ is minimal in $\beta$. Here, $\lessdot$ denotes the covering relation, meaning $x \lessdot y$ if $x < y$ and there is no $z$ such that $x < z < y$.

Prod.Lex.covBy_iff theorem

 {a b : α ×ₗ β} :
  a ⋖ b ↔
    (ofLex a).1 = (ofLex b).1 ∧ (ofLex a).2 ⋖ (ofLex b).2 ∨
      (ofLex a).1 ⋖ (ofLex b).1 ∧ IsMax (ofLex a).2 ∧ IsMin (ofLex b).2

Full source

theorem covBy_iff {a b : α ×ₗ β} :
    a ⋖ ba ⋖ b ↔ (ofLex a).1 = (ofLex b).1 ∧ (ofLex a).2 ⋖ (ofLex b).2 ∨
      (ofLex a).1 ⋖ (ofLex b).1 ∧ IsMax (ofLex a).2 ∧ IsMin (ofLex b).2 :=
  toLex_covBy_toLex_iff

Characterization of Covering Relation in Lexicographic Order

Informal description

Let $\alpha$ and $\beta$ be types equipped with strict orders, and let $a, b$ be elements of the lexicographically ordered product $\alpha \times_\ell \beta$. Then $a \lessdot b$ holds if and only if either: 1. The first components are equal ($(\text{ofLex } a).1 = (\text{ofLex } b).1$) and the second components satisfy $(\text{ofLex } a).2 \lessdot (\text{ofLex } b).2$ in $\beta$, or 2. The first components satisfy $(\text{ofLex } a).1 \lessdot (\text{ofLex } b).1$ in $\alpha$, while $(\text{ofLex } a).2$ is maximal in $\beta$ and $(\text{ofLex } b).2$ is minimal in $\beta$. Here, $\lessdot$ denotes the covering relation, meaning $x \lessdot y$ if $x < y$ and there is no $z$ such that $x < z < y$.

Prod.Lex.toLex_le_toLex' theorem

: toLex x ≤ toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)

Full source

/-- Variant of `Prod.Lex.toLex_le_toLex` for partial orders. -/
lemma toLex_le_toLex' : toLextoLex x ≤ toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2) := by
  simp only [toLex_le_toLex, lt_iff_le_not_le, le_antisymm_iff]
  tauto

Lexicographic Order Inequality: $\text{toLex}(x) \leq \text{toLex}(y) \leftrightarrow (a_1 \leq a_2) \land (a_1 = a_2 \to b_1 \leq b_2)$

Informal description

For any two elements $x = (a_1, b_1)$ and $y = (a_2, b_2)$ in the lexicographically ordered product $\alpha \times_\ell \beta$, the inequality $\text{toLex}(x) \leq \text{toLex}(y)$ holds if and only if $a_1 \leq a_2$ and whenever $a_1 = a_2$, then $b_1 \leq b_2$.

Prod.Lex.toLex_lt_toLex' theorem

: toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Full source

/-- Variant of `Prod.Lex.toLex_lt_toLex` for partial orders. -/
lemma toLex_lt_toLex' : toLextoLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2) := by
  rw [toLex_lt_toLex]
  simp only [lt_iff_le_not_le, le_antisymm_iff]
  tauto

Characterization of Strict Lexicographic Order via Componentwise Comparison

Informal description

For any two elements $x = (a_1, b_1)$ and $y = (a_2, b_2)$ in the lexicographically ordered product $\alpha \times_\ell \beta$, the strict inequality $\text{toLex}(x) < \text{toLex}(y)$ holds if and only if $a_1 \leq a_2$ and whenever $a_1 = a_2$, then $b_1 < b_2$.

Prod.Lex.le_iff' theorem

 {x y : α ×ₗ β} : x ≤ y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 ≤ (ofLex y).2)

Full source

/-- Variant of `Prod.Lex.le_iff` for partial orders. -/
lemma le_iff' {x y : α ×ₗ β} :
    x ≤ y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 ≤ (ofLex y).2) :=
  toLex_le_toLex'

Characterization of Lexicographic Order Inequality via Componentwise Comparison

Informal description

For any two elements $x$ and $y$ in the lexicographically ordered product $\alpha \times_\ell \beta$, the inequality $x \leq y$ holds if and only if the first component of $x$ is less than or equal to the first component of $y$, and whenever the first components are equal, the second component of $x$ is less than or equal to the second component of $y$.

Prod.Lex.lt_iff' theorem

 {x y : α ×ₗ β} : x < y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 < (ofLex y).2)

Full source

/-- Variant of `Prod.Lex.lt_iff` for partial orders. -/
lemma lt_iff' {x y : α ×ₗ β} :
    x < y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 < (ofLex y).2) :=
  toLex_lt_toLex'

Characterization of Strict Lexicographic Order via Componentwise Comparison

Informal description

For any two elements $x = (a_1, b_1)$ and $y = (a_2, b_2)$ in the lexicographically ordered product $\alpha \times_\ell \beta$, the strict inequality $x < y$ holds if and only if $a_1 \leq a_2$ and whenever $a_1 = a_2$, then $b_1 < b_2$.

Prod.Lex.toLex_mono theorem

: Monotone (toLex : α × β → α ×ₗ β)

Full source

theorem toLex_mono : Monotone (toLex : α × β → α ×ₗ β) :=
  fun _x _y hxy ↦ toLex_le_toLex'.2 ⟨hxy.1, fun _ ↦ hxy.2⟩

Monotonicity of Lexicographic Order Embedding

Informal description

The function $\text{toLex} : \alpha \times \beta \to \alpha \times_\ell \beta$, which maps a pair to its lexicographically ordered counterpart, is monotone. That is, for any pairs $(a_1, b_1)$ and $(a_2, b_2)$ in $\alpha \times \beta$, if $(a_1, b_1) \leq (a_2, b_2)$ in the product order, then $\text{toLex}(a_1, b_1) \leq \text{toLex}(a_2, b_2)$ in the lexicographic order.

Prod.Lex.toLex_strictMono theorem

: StrictMono (toLex : α × β → α ×ₗ β)

Full source

theorem toLex_strictMono : StrictMono (toLex : α × β → α ×ₗ β) := by
  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
  obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt
  · exact right _ (Prod.mk_lt_mk_iff_right.1 h)
  · exact left _ _ ha

Strict Monotonicity of Lexicographic Order Embedding

Informal description

The function `toLex` from the product type $\alpha \times \beta$ to the lexicographically ordered product type $\alpha \times_\ell \beta$ is strictly monotone. That is, for any pairs $(a_1, b_1)$ and $(a_2, b_2)$ in $\alpha \times \beta$, if $(a_1, b_1) < (a_2, b_2)$ in the lexicographic order, then `toLex $(a_1, b_1)$ < toLex $(a_2, b_2)$` holds in $\alpha \times_\ell \beta$.

Prod.Lex.instPartialOrder instance

(α β : Type*) [PartialOrder α] [PartialOrder β] : PartialOrder (α ×ₗ β)

Full source

/-- Dictionary / lexicographic partial order for pairs. -/
instance instPartialOrder (α β : Type*) [PartialOrder α] [PartialOrder β] :
    PartialOrder (α ×ₗ β) where
  le_antisymm _ _ := antisymm_of (Prod.Lex _ _)

Lexicographic Partial Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with partial orders, the lexicographic product $\alpha \times_\ell \beta$ is also equipped with a partial order. The order relation is defined by $(a_1, b_1) \leq (a_2, b_2)$ if and only if either $a_1 < a_2$ or ($a_1 = a_2$ and $b_1 \leq b_2$).

Prod.Lex.instOrdLexProd instance

[Ord α] [Ord β] : Ord (α ×ₗ β)

Full source

instance instOrdLexProd [Ord α] [Ord β] : Ord (α ×ₗ β) := lexOrd

Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with order structures, the lexicographic product $\alpha \times_\ell \beta$ inherits an order structure where $(a_1, b_1) \leq (a_2, b_2)$ if either $a_1 < a_2$ or ($a_1 = a_2$ and $b_1 \leq b_2$).

Prod.Lex.compare_def theorem

 [Ord α] [Ord β] : @compare (α ×ₗ β) _ = compareLex (compareOn fun x => (ofLex x).1) (compareOn fun x => (ofLex x).2)

Full source

theorem compare_def [Ord α] [Ord β] : @compare (α ×ₗ β) _ =
    compareLex (compareOn fun x => (ofLex x).1) (compareOn fun x => (ofLex x).2) := rfl

Lexicographic Comparison Definition for Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with order structures, the comparison function on the lexicographic product $\alpha \times_\ell \beta$ is defined as the lexicographic comparison of the projections onto $\alpha$ and $\beta$. Specifically, for $(a_1, b_1), (a_2, b_2) \in \alpha \times_\ell \beta$, the comparison is given by first comparing $a_1$ and $a_2$ using $\alpha$'s order, and if they are equal, comparing $b_1$ and $b_2$ using $\beta$'s order.

lexOrd_eq theorem

[Ord α] [Ord β] : @lexOrd α β _ _ = instOrdLexProd

Full source

theorem _root_.lexOrd_eq [Ord α] [Ord β] : @lexOrd α β _ _ = instOrdLexProd := rfl

Equality of Lexicographic Order Constructions on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with order structures, the lexicographic order `lexOrd` on $\alpha \times \beta$ is equal to the lexicographic product order instance `instOrdLexProd` on $\alpha \times_\ell \beta$.

Ord.lex_eq theorem

[oα : Ord α] [oβ : Ord β] : Ord.lex oα oβ = instOrdLexProd

Full source

theorem _root_.Ord.lex_eq [oα : Ord α] [oβ : Ord β] : Ord.lex oα oβ = instOrdLexProd := rfl

Lexicographic Order Construction Equals Product Lex Order Instance

Informal description

For any types $\alpha$ and $\beta$ with order structures `oα` and `oβ` respectively, the lexicographic order construction `Ord.lex oα oβ` is equal to the lexicographic order instance `instOrdLexProd` on the product type $\alpha \times_\ell \beta$.

Prod.Lex.instOrientedOrdLex instance

[Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] : OrientedOrd (α ×ₗ β)

Full source

instance [Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] : OrientedOrd (α ×ₗ β) :=
  inferInstanceAs (OrientedCmp (compareLex _ _))

Orientation of Lexicographic Product Order

Informal description

For any types $\alpha$ and $\beta$ equipped with order structures and orientation properties, the lexicographic product $\alpha \times_\ell \beta$ inherits an orientation property. This means that the lexicographic order on $\alpha \times \beta$ respects the orientation of the individual orders on $\alpha$ and $\beta$.

Prod.Lex.instTransOrdLex instance

[Ord α] [Ord β] [TransOrd α] [TransOrd β] : TransOrd (α ×ₗ β)

Full source

instance [Ord α] [Ord β] [TransOrd α] [TransOrd β] : TransOrd (α ×ₗ β) :=
  inferInstanceAs (TransCmp (compareLex _ _))

Transitivity of Lexicographic Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with transitive order structures, the lexicographic product $\alpha \times_\ell \beta$ also forms a transitive order. Here, the lexicographic order on $\alpha \times_\ell \beta$ is defined such that $(a_1, b_1) \leq (a_2, b_2)$ if either $a_1 < a_2$ or ($a_1 = a_2$ and $b_1 \leq b_2$).

Prod.Lex.instLinearOrder instance

(α β : Type*) [LinearOrder α] [LinearOrder β] : LinearOrder (α ×ₗ β)

Full source

/-- Dictionary / lexicographic linear order for pairs. -/
instance instLinearOrder (α β : Type*) [LinearOrder α] [LinearOrder β] : LinearOrder (α ×ₗ β) :=
  { Prod.Lex.instPartialOrder α β with
    le_total := total_of (Prod.Lex _ _)
    toDecidableLE := Prod.Lex.decidable _ _
    toDecidableLT := Prod.Lex.decidable _ _
    toDecidableEq := instDecidableEqLex _
    compare_eq_compareOfLessAndEq := fun a b => by
      have : DecidableLT (α ×ₗ β) := Prod.Lex.decidable _ _
      have : BEqOrd (α ×ₗ β) := ⟨by
        simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq, compare_eq_iff_eq]⟩
      have : LTOrd (α ×ₗ β) := ⟨by
        simp [compare_def, compareLex, compareOn, Ordering.then_eq_lt, toLex_lt_toLex,
          compare_lt_iff_lt, compare_eq_iff_eq]⟩
      convert LTCmp.eq_compareOfLessAndEq (cmp := compare) a b }

Lexicographic Linear Order on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with linear orders, the lexicographic product $\alpha \times_\ell \beta$ is also equipped with a linear order. The order relation is defined by $(a_1, b_1) \leq (a_2, b_2)$ if and only if either $a_1 < a_2$ or ($a_1 = a_2$ and $b_1 \leq b_2$).

Prod.Lex.orderBot instance

[PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] : OrderBot (α ×ₗ β)

Full source

instance orderBot [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] : OrderBot (α ×ₗ β) where
  bot := toLex ⊥
  bot_le _ := toLex_mono bot_le

Bottom Element in Lexicographic Product Order

Informal description

For any types $\alpha$ and $\beta$ equipped with partial order and preorder structures respectively, and each having a least element $\bot$, the lexicographic product $\alpha \times_\ell \beta$ also has a least element. The bottom element in $\alpha \times_\ell \beta$ is given by $(\bot, \bot)$, and it satisfies the property that $(\bot, \bot) \leq (a, b)$ for any $(a, b) \in \alpha \times_\ell \beta$.

Prod.Lex.orderTop instance

[PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] : OrderTop (α ×ₗ β)

Full source

instance orderTop [PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] : OrderTop (α ×ₗ β) where
  top := toLex ⊤
  le_top _ := toLex_mono le_top

Top Element in Lexicographic Product Order

Informal description

For any types $\alpha$ and $\beta$ equipped with a partial order and a preorder respectively, and each having a greatest element $\top$, the lexicographic product $\alpha \times_\ell \beta$ also has a greatest element. The top element in $\alpha \times_\ell \beta$ is given by $(\top, \top)$, and it satisfies the property that $(a, b) \leq (\top, \top)$ for any $(a, b) \in \alpha \times_\ell \beta$.

Prod.Lex.boundedOrder instance

[PartialOrder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] : BoundedOrder (α ×ₗ β)

Full source

instance boundedOrder [PartialOrder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] :
    BoundedOrder (α ×ₗ β) :=
  { Lex.orderBot, Lex.orderTop with }

Bounded Lexicographic Product Order

Informal description

For any partially ordered set $\alpha$ and preordered set $\beta$ that are both bounded (i.e., have both a greatest element $\top$ and a least element $\bot$), the lexicographic product $\alpha \times_\ell \beta$ is also a bounded order. The greatest element is $(\top, \top)$ and the least element is $(\bot, \bot)$.

Prod.Lex.instDenselyOrderedLex instance

[Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] : DenselyOrdered (α ×ₗ β)

Full source

instance [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] :
    DenselyOrdered (α ×ₗ β) where
  dense := by
    rintro _ _ (@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩)
    · obtain ⟨c, h₁, h₂⟩ := exists_between h
      exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := exists_between h
      exact ⟨(a, c), right _ h₁, right _ h₂⟩

Densely Ordered Lexicographic Product of Preorders

Informal description

For any preorders $\alpha$ and $\beta$ that are densely ordered, the lexicographic product $\alpha \times_\ell \beta$ is also densely ordered. This means that for any two pairs $(a_1, b_1) < (a_2, b_2)$ in $\alpha \times_\ell \beta$, there exists a pair $(a, b)$ such that $(a_1, b_1) < (a, b) < (a_2, b_2)$.

Prod.Lex.noMaxOrder_of_left instance

[Preorder α] [Preorder β] [NoMaxOrder α] : NoMaxOrder (α ×ₗ β)

Full source

instance noMaxOrder_of_left [Preorder α] [Preorder β] [NoMaxOrder α] : NoMaxOrder (α ×ₗ β) where
  exists_gt := by
    rintro ⟨a, b⟩
    obtain ⟨c, h⟩ := exists_gt a
    exact ⟨⟨c, b⟩, left _ _ h⟩

Lexicographic Product Preserves No Maximal Elements from Left Factor

Informal description

For any preorders $\alpha$ and $\beta$, if $\alpha$ has no maximal elements, then the lexicographic product $\alpha \times_\ell \beta$ also has no maximal elements.

Prod.Lex.noMinOrder_of_left instance

[Preorder α] [Preorder β] [NoMinOrder α] : NoMinOrder (α ×ₗ β)

Full source

instance noMinOrder_of_left [Preorder α] [Preorder β] [NoMinOrder α] : NoMinOrder (α ×ₗ β) where
  exists_lt := by
    rintro ⟨a, b⟩
    obtain ⟨c, h⟩ := exists_lt a
    exact ⟨⟨c, b⟩, left _ _ h⟩

No Minimal Elements in Lexicographic Product from Left Factor

Informal description

For any preorders $\alpha$ and $\beta$, if $\alpha$ has no minimal elements, then the lexicographic product $\alpha \times_\ell \beta$ also has no minimal elements.

Prod.Lex.noMaxOrder_of_right instance

[Preorder α] [Preorder β] [NoMaxOrder β] : NoMaxOrder (α ×ₗ β)

Full source

instance noMaxOrder_of_right [Preorder α] [Preorder β] [NoMaxOrder β] : NoMaxOrder (α ×ₗ β) where
  exists_gt := by
    rintro ⟨a, b⟩
    obtain ⟨c, h⟩ := exists_gt b
    exact ⟨⟨a, c⟩, right _ h⟩

Lexicographic Product Preserves No Maximal Elements from Right Factor

Informal description

For any preorders $\alpha$ and $\beta$, if $\beta$ has no maximal elements, then the lexicographic product $\alpha \times_\ell \beta$ also has no maximal elements.

Prod.Lex.noMinOrder_of_right instance

[Preorder α] [Preorder β] [NoMinOrder β] : NoMinOrder (α ×ₗ β)

Full source

instance noMinOrder_of_right [Preorder α] [Preorder β] [NoMinOrder β] : NoMinOrder (α ×ₗ β) where
  exists_lt := by
    rintro ⟨a, b⟩
    obtain ⟨c, h⟩ := exists_lt b
    exact ⟨⟨a, c⟩, right _ h⟩

No Minimal Elements in Lexicographic Product from Right Factor

Informal description

For any preorders $\alpha$ and $\beta$, if $\beta$ has no minimal elements, then the lexicographic product $\alpha \times_\ell \beta$ also has no minimal elements.

Mathlib.Data.Prod.Lex

Main declarations

Notation

See also