English
If s is connected, bounded below, bounded above, and closed, then s is exactly the closed interval between its infimum and supremum.
Русский
Если s связано, ограничено снизу и сверху и замкнуто, то s ровно равно Icc(Inf s, Sup s).
LaTeX
$$$IsConnected(s) \land BddBelow(s) \land BddAbove(s) \land IsClosed(s) \Rightarrow s = Icc(sInf(s), sSup(s))$$$
Lean4
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `b`, and for any `a ≤ y < x ≤ b`, `x ∈ s`, the set `s ∩ [y, x)`
is not empty, then `[a, b] ⊆ s`. -/
theorem Icc_subset_of_forall_exists_lt {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (hb : b ∈ s)
(hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty) : Icc a b ⊆ s :=
by
intro y hy
have : IsClosed (s ∩ Icc y b) :=
by
suffices s ∩ Icc y b = s ∩ Icc a b ∩ Icc y b from this ▸ hs.inter isClosed_Icc
grind [Icc_subset_Icc_left, inter_eq_self_of_subset_right, inter_assoc]
exact
IsClosed.mem_of_ge_of_forall_exists_lt this hb hy.2 fun x hx ↦ hgt x ⟨hx.1, Ioc_subset_Ioc_left hy.1 hx.2⟩ y hx.2.1
