nhdsWithin_insert — Mathlib

English

The neighborhood within insert a s at a is the supremum of the pure neighborhood at a and the nhdsWithin a s.

Русский

Окрестность внутри вставки a в s равна объединению (супремуму) чистой окрестности в a и 𝓝[a] внутри s.

LaTeX

$$$$ 𝓝[\\operatorname{insert}(a,s)] a = \\mathcal{N}_{a}^{\\text{pure}} \\sqcup 𝓝[a]_{s} $$$$

Lean4

@[simp]
theorem nhdsWithin_insert (a : α) (s : Set α) : 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a := by
  rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]

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