nhdsWithin_coe — Mathlib

English

For any subset s of OnePoint X and any x ∈ X, the nhdsWithin at ι(x) relative to ι^{-1}'s image equals the pushforward of nhdsWithin at x by ι.

Русский

Для точки x∈X в OnePoint X окрестности в ι(x) относительно образа ι^{-1} совпадают с отображением окрестностей x в X через вложение.

LaTeX

$$$\mathcal{N}_{(\uparrow) s}(\uparrow x) = \operatorname{map}(\uparrow)(\mathcal{N}_{(\uparrow)^{-1}' s} x),$$$

Lean4

theorem nhdsWithin_coe (s : Set (OnePoint X)) (x : X) : 𝓝[s] ↑x = map (↑) (𝓝[(↑) ⁻¹' s] x) :=
  (isOpenEmbedding_coe.map_nhdsWithin_preimage_eq _ _).symm

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