denselyOrdered_of_noMinOrder — Mathlib

English

If ι is densely ordered, α(i) densely ordered, and NoMinOrder on α(i), then Lex is densely ordered.

Русский

Если ι densely ordered, α(i) densely ordered, и NoMinOrder на α(i), то Lex densely ordered.

LaTeX

$$$\text{DenselyOrdered}(\Sigma_\text{Lex} i, α(i))$ under NoMinOrder assumptions.$$

Lean4

instance denselyOrdered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)] [∀ i, DenselyOrdered (α i)]
    [∀ i, NoMinOrder (α i)] : DenselyOrdered (Σₗ i, α i) where
  dense := by
    rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | ⟨_, b, h⟩)
    · obtain ⟨c, hb⟩ := exists_lt b
      exact ⟨⟨j, c⟩, left _ _ h, right _ _ hb⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩

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