English
In a discrete subset s, there exists a punctured neighborhood U of x (U ≠ ∅ around x) disjoint from s.
Русский
Для дискретного подмножества s существует непустое окружение U вокруг x такое, что U ∩ s = ∅.
LaTeX
$$$ {s : Set X} [DiscreteTopology s] {x : X} (hx : x \\in s) : \\exists U \\in 𝓝[\\neq] x, Disjoint U s. $$$
Lean4
/-- For point `x` in a discrete subset `s` of a topological space, there is a set `U`
such that
1. `U` is a punctured neighborhood of `x` (i.e. `U ∪ {x}` is a neighbourhood of `x`),
2. `U` is disjoint from `s`.
-/
theorem disjoint_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) :
∃ U ∈ 𝓝[≠] x, Disjoint U s :=
let ⟨V, h, h'⟩ := nhds_inter_eq_singleton_of_mem_discrete hx
⟨{ x }ᶜ ∩ V, inter_mem_nhdsWithin _ h, disjoint_iff_inter_eq_empty.mpr (by rw [inter_assoc, h', compl_inter_self])⟩
