English
Let X be a topological space and s ⊆ X. A set s is closed if and only if every point a that is a cluster point of s (i.e., belongs to the closure of s) actually lies in s.
Русский
Пусть X — топологическое пространство и s ⊆ X. Множество s замкнуто тогда и только тогда, когда любая точка a, являющаяся кластерной точкой множества s (то есть принадлежит замыканию s), принадлежит самому s.
LaTeX
$$$ IsClosed\\,(s) \\iff \\forall a,\\, ClusterPt\\,a\\,(\\mathcal{P} s) \\to a \\in s $$$
Lean4
theorem isClosed_iff_clusterPt : IsClosed s ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s :=
calc
IsClosed s ↔ closure s ⊆ s := closure_subset_iff_isClosed.symm
_ ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s := by simp only [subset_def, mem_closure_iff_clusterPt]
