English
A preconnected set is order-connected.
Русский
Предсвязное множество является связным по порядку.
LaTeX
$$$IsPreconnected(s) \Rightarrow OrdConnected(s)$$$
Lean4
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `a ≤ x < y ≤ b`, `x ∈ s`, the set `s ∩ (x, y]`
is not empty, then `[a, b] ⊆ s`. -/
theorem Icc_subset_of_forall_exists_gt {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s)
(hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty) : Icc a b ⊆ s :=
by
intro y hy
have : IsClosed (s ∩ Icc a y) :=
by
suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y from this ▸ hs.inter isClosed_Icc
grind [inter_assoc, inter_eq_self_of_subset_right, Icc_subset_Icc_right]
exact
IsClosed.mem_of_ge_of_forall_exists_gt this ha hy.1 fun x hx ↦ hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2
