nhdsSet_insert — Mathlib

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. -/

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