denselyOrdered_of_noMinOrder — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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