denselyOrdered_set_iff_subsingleton

English

Let X be a type with a linear order and locally finite order. For any subset s of WithZero X, s is densely ordered if and only if s is subsingleton (contains at most one element).

Русский

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

LaTeX

$$$DenselyOrdered\\,s \\iff (\\forall a,b\\in s,\ a=b)$$$

Lean4

theorem denselyOrdered_set_iff_subsingleton {X : Type*} [LinearOrder X] [LocallyFiniteOrder X] {s : Set (WithZero X)} :
    DenselyOrdered s ↔ s.Subsingleton :=
  WithBot.denselyOrdered_set_iff_subsingleton

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