English
For a densely ordered α, a preconnected s is contained in one of the standard interval types.
Русский
Для плотно упорядоченного α предсвязное s содержится в одном из стандартных типов интервалов.
LaTeX
$$$\text{IsPreconnected}(s) \Rightarrow s \in \{Icc, Ico, Ioc, Ioo, Ici, Ioi, Iic, Iio, univ, \emptyset\}$$$
Lean4
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `b`, and the set `s ∩ (a, b]` has no minimal point, then `a ∈ s`. -/
theorem mem_of_ge_of_forall_exists_lt {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (hb : b ∈ s) (hab : a ≤ b)
(hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty) : a ∈ s :=
by
suffices OrderDual.toDual a ∈ ofDual ⁻¹' s by aesop
have : IsClosed (OrderDual.ofDual ⁻¹' (s ∩ Icc a b)) := hs
rw [preimage_inter, ← Icc_toDual] at this
apply this.mem_of_ge_of_forall_exists_gt (by aesop) (by aesop) (fun x hx ↦ ?_)
rw [Ico_toDual, ← preimage_inter, preimage_equiv_eq_image_symm, mem_image] at hx
aesop
