denselyOrdered_of_noMaxOrder — Mathlib

English

If ι is densely ordered, α(i) are densely ordered, and NoMaxOrder on each α(i), then Lex is densely ordered.

Русский

Если ι плотно упорядочен, α(i) плотно упорядочены, и у каждого α(i) есть NoMaxOrder, то Lex плотно упорядочен.

LaTeX

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

Lean4

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

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