denselyOrdered_iff_subsingleton — Mathlib

English

Let X be a linearly ordered set with LocallyFiniteOrder. Then X is densely ordered if and only if X is subsingleton.

Русский

Пусть X — линейно упорядоченное множество с локально конечной структурой. Тогда X плотно упорядочено тогда и только тогда, когда X является одиночным множеством.

LaTeX

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

Lean4

theorem denselyOrdered_iff_subsingleton : DenselyOrdered X ↔ Subsingleton X :=
  by
  refine ⟨fun H ↦ ?_, fun h ↦ h.instDenselyOrdered⟩
  rw [← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]
  rintro ⟨a, b, hab⟩
  exact not_lt_of_denselyOrdered_of_locallyFinite a b hab

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