denselyOrdered_of_noMaxOrder — Mathlib

English

If ι is densely ordered, α_i are densely ordered with no maximum, then Σₗ' i, α_i is densely ordered.

Русский

Если ι плотно упорядочено, α_i плотно упорядочены и не имеют максимального элемента, то Σₗ' i, α_i плотно упорядочен.

LaTeX

$$$\\text{DenselyOrdered}(\\Sigma'_i,\\alpha_i)$$$

Lean4

instance denselyOrdered_of_noMaxOrder [Preorder ι] [∀ i, Preorder (α i)] [∀ i, DenselyOrdered (α i)]
    [∀ i, NoMaxOrder (α i)] : DenselyOrdered (Σₗ' i, α i) :=
  ⟨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⟩⟩

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