English
Let α be a densely ordered, conditionally complete linear order with the order topology. Then for every subset s ⊆ α, IsPreconnected s if and only if OrdConnected s.
Русский
Пусть α — плотное условно полно упорядоченное линейное множество с порядковой топологией. Тогда для любого подмножества s ⊆ α выполняется: s предсоединовано тогда и только тогда, когда оно упорядочно связно.
LaTeX
$$$IsPreconnected\\ s \\iff OrdConnected\\ s$$$
Lean4
theorem isPreconnected_iff_ordConnected {s : Set α} : IsPreconnected s ↔ OrdConnected s :=
⟨IsPreconnected.ordConnected, Set.OrdConnected.isPreconnected⟩