nhdsWithin_coe_image — Mathlib

English

For any subset s of X and any x ∈ X, the nhdsWithin of x in the image ι''s equals the map of the nhdsWithin of x in s along the embedding ι.

Русский

Для подмножества s ⊆ X и x ∈ X окрестности точки x вдоль образа ι''s эквивалентны отображению окрестностей x в s через вложение ι.

LaTeX

$$$\mathcal{N}_{(\uparrow)''s}(\uparrow x) = \operatorname{map}(\uparrow)(\mathcal{N}_{s} x),$ for all $s\subset X$ and $x\in X$.$$

Lean4

theorem nhdsWithin_coe_image (s : Set X) (x : X) : 𝓝[(↑) '' s] (x : OnePoint X) = map (↑) (𝓝[s] x) :=
  (isOpenEmbedding_coe.isEmbedding.map_nhdsWithin_eq _ _).symm

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