nhdsSet_nhdsKer — Mathlib

English

The set neighborhood of the kernel equals the set neighborhood of the set: nhdsSet(nhdsKer(s)) = nhdsSet(s).

Русский

Окружение на уровне множеств ядра совпадает с окружением на уровне самого множества: nhdsSet(nhdsKer(s)) = nhdsSet(s).

LaTeX

$$$nhdsSet(nhdsKer(s)) = nhdsSet(s)$$$

Lean4

@[simp]
theorem nhdsSet_nhdsKer (s : Set X) : 𝓝ˢ (nhdsKer s) = 𝓝ˢ s :=
  by
  refine le_antisymm ((hasBasis_nhdsSet _).ge_iff.2 ?_) (nhdsSet_mono subset_nhdsKer)
  exact fun U ⟨hUo, hsU⟩ ↦ hUo.mem_nhdsSet.2 <| hUo.nhdsKer_subset.2 hsU

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