English
A subset S is closed and discrete if and only if for every x ∈ X, the punctured neighborhood around x is disjoint from S as a principal filter, i.e., S is isolated at each point.
Русский
Подмножество S замкнуто и дискретно тогда и только тогда, когда для каждого x ∈ X окрестности вокруг x, удалив x, не пересекают S как фильтр-проница, т.е. точки из S изолированы во всех точках.
LaTeX
$$$\\text{IsClosed } S \\land \\mathrm{DiscreteTopology } S \\iff \\forall x, \\ Disjoint (\\mathcal{N}_{=}^{x}) (\\mathscr{P}S)$$$
Lean4
/-- Criterion for a subset `S ⊆ X` to be closed and discrete in terms of the punctured
neighbourhood filter at an arbitrary point of `X`. (Compare `discreteTopology_subtype_iff`.) -/
theorem isClosed_and_discrete_iff {S : Set X} : IsClosed S ∧ DiscreteTopology S ↔ ∀ x, Disjoint (𝓝[≠] x) (𝓟 S) :=
by
rw [discreteTopology_subtype_iff, isClosed_iff_clusterPt, ← forall_and]
congrm (∀ x, ?_)
rw [← not_imp_not, clusterPt_iff_not_disjoint, not_not, ← disjoint_iff]
constructor <;> intro H
· by_cases hx : x ∈ S
exacts [H.2 hx, (H.1 hx).mono_left nhdsWithin_le_nhds]
· refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩
simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H
