denselyOrdered_set_iff_subsingleton

English

Let X be a linear order with LocallyFiniteOrder. For any s ⊆ WithTop X, the induced order on s is densely ordered iff s is subsingleton.

Русский

Пусть X — линейно упорядоченное множество с LocallyFiniteOrder. Для любого подмножества s ⊆ WithTop X соответствующий порядок плотно упорядочен тогда и только тогда, когда s является одиночным.

LaTeX

$$$\mathrm{DenselyOrdered}(s) \iff \mathrm{Subsingleton}(s).$$$

Lean4

theorem denselyOrdered_set_iff_subsingleton {s : Set (WithTop X)} : DenselyOrdered s ↔ s.Subsingleton :=
  by
  have he : StrictAnti (WithTop.toDual.image s) := WithTop.toDual.image_strictAnti _ (fun ⦃a b⦄ a ↦ a)
  rw [denselyOrdered_iff_of_strictAnti _ he, WithBot.denselyOrdered_set_iff_subsingleton,
    WithTop.toDual.injective.subsingleton_image_iff]

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