English
A closed interval is preconnected in a densely ordered conditionally complete linear order.
Русский
Замкнутый интервал является предсвязным в плотно упорядоченном условно полноценно упорядоченном отношении.
LaTeX
$$$IsPreconnected(Icc(a,b))$$$
Lean4
/-- A closed interval in a densely ordered conditionally complete linear order is preconnected. -/
theorem isPreconnected_Icc : IsPreconnected (Icc a b) :=
isPreconnected_closed_iff.2
(by
rintro s t hs ht hab ⟨x, hx⟩
⟨y, hy⟩
-- This used to use `wlog`, but it was causing timeouts.
rcases le_total x y with h | h
· exact isPreconnected_Icc_aux x y s t h hs ht hab hx hy
· rw [inter_comm s t]
rw [union_comm s t] at hab
exact isPreconnected_Icc_aux y x t s h ht hs hab hy hx)
