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