denselyOrdered_set_iff_subsingleton

English

In a locally finite linear order X, for any subset s of X, the induced order on s is densely ordered if and only if s is subsingleton.

Русский

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

LaTeX

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

Lean4

theorem denselyOrdered_set_iff_subsingleton {s : Set X} : DenselyOrdered s ↔ s.Subsingleton := by
  classical simp [LocallyFiniteOrder.denselyOrdered_iff_subsingleton]

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