English
The collection of all preconnected sets is contained in the union of a finite list of canonical interval types (and ∅, univ).
Русский
Множество всех предсоединённых множеств содержится в объединении конечного набора канонических типов интервалов (и ∅, univ).
LaTeX
$$$\{ s : Set(\alpha) \mid IsPreconnected(s) \} \subseteq \big( \text{ranges of } Icc,Ico,Ioc,Ioo,Ici,Ioi,Iic,Iio,univ,\emptyset \big)$$$
Lean4
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and the set `s ∩ [a, b)` has no maximal point, then `b ∈ s`. -/
theorem mem_of_ge_of_forall_exists_gt {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s) (hab : a ≤ b)
(hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty) : b ∈ s :=
by
let S := s ∩ Icc a b
replace ha : a ∈ S := ⟨ha, left_mem_Icc.2 hab⟩
have Sbd : BddAbove S := ⟨b, fun z hz => hz.2.2⟩
let c := sSup (s ∩ Icc a b)
have c_mem : c ∈ S := hs.csSup_mem ⟨_, ha⟩ Sbd
have c_le : c ≤ b := csSup_le ⟨_, ha⟩ fun x hx => hx.2.2
rcases eq_or_lt_of_le c_le with hc | hc
· exact hc ▸ c_mem.1
exfalso
rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩
exact not_lt_of_ge (le_csSup Sbd ⟨xs, le_trans (le_csSup Sbd ha) (le_of_lt cx), xb⟩) cx
