English
A preconnected set in a densely ordered conditionally complete linear order must be one of the standard interval types (including unbounded and undecorated cases).
Русский
Предсоединённое множество в плотном линейном порядке принадлежит одному из стандартных типов интервалов.
LaTeX
$$$IsPreconnected(s) \Rightarrow s \in \{Icc(sInf(s), sSup(s)), Ico(sInf(s), sSup(s)), Ioc(sInf(s), sSup(s)), Ioo(sInf(s), sSup(s)), Ici(sInf(s)), Ioi(sInf(s)), Iic(sSup(s)), Iio(sSup(s)), univ, \emptyset\}$$$
Lean4
theorem Ioi_csInf_subset {s : Set α} (hs : IsPreconnected s) (hb : BddBelow s) (ha : ¬BddAbove s) : Ioi (sInf s) ⊆ s :=
fun x hx =>
have sne : s.Nonempty := nonempty_of_not_bddAbove ha
let ⟨_y, ys, hy⟩ : ∃ y ∈ s, y < x := (isGLB_lt_iff (isGLB_csInf sne hb)).1 hx
let ⟨_z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x
hs.Icc_subset ys zs ⟨hy.le, hz.le⟩
