instDenselyOrdered — Mathlib

English

If every α(i) is densely ordered and each α(i) is a nonempty preorder, then the lexicographic order on the sigma-type Lex ((i) × α(i)) is densely ordered.

Русский

Если для каждого i множество α(i) представлено плотным порядком, и каждое α(i) непусто, то лексикографический порядок на сигма-помещении Lex ((i) × α(i)) является плотно упорядоченным.

LaTeX

$$$\text{DenselyOrdered}(\Sigma_\text{Lex} i, α(i))$$$

Lean4

instance [∀ i, Preorder (α i)] [∀ i, DenselyOrdered (α i)] : DenselyOrdered (Σ i, α i) where
  dense := by
    rintro ⟨i, a⟩ ⟨_, _⟩ ⟨_, _, b, h⟩
    obtain ⟨c, ha, hb⟩ := exists_between h
    exact ⟨⟨i, c⟩, LT.fiber i a c ha, LT.fiber i c b hb⟩

Похожие утверждения