English
The set-neighborhoods of an inserted point x into s equals the join of 𝓝ˢ s with 𝓝 x.
Русский
Окрестности x, добавленного к s, равны объединению 𝓝 x и 𝓝ˢ s.
LaTeX
$$$ 𝓝ˢ (\text{insert } x\, s) = 𝓝 x \sqcup 𝓝ˢ s $$$
Lean4
@[simp]
theorem nhdsSet_insert (x : X) (s : Set X) : 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s := by
rw [insert_eq, nhdsSet_union, nhdsSet_singleton]
/- This inequality cannot be improved to an equality. For instance,
if `X` has two elements and the coarse topology and `s` and `t` are distinct singletons then
`𝓝ˢ (s ∩ t) = ⊥` while `𝓝ˢ s ⊓ 𝓝ˢ t = ⊤` and those are different. -/