Icc_subset_of_forall_mem_nhdsWithin

English

If s is connected, bounded below, bounded above, and closed, then s equals the closed interval between its Inf and Sup.

Русский

Если s связано, ограничено снизу и сверху и замкнуто, то s равно [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 `a`, and for any `x ∈ s ∩ [a, b)` the set `s` includes some open
neighborhood of `x` within `(x, +∞)`, then `[a, b] ⊆ s`. -/
theorem Icc_subset_of_forall_mem_nhdsWithin {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s)
    (hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x) : Icc a b ⊆ s :=
  hs.Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset ha (fun _t ht h't ↦ hgt _ ⟨h't ⟨ht.1, le_rfl⟩, ht⟩)

Похожие утверждения