English
For an open embedding f and any s ⊆ β, the pushforward of the nhds within by f along x is equal to nhdsWithin at f x on the preimage s.
Русский
Для открытого вложения f и любой s ⊆ β, образ nhdsWithin по f вдоль x равен nhdsWithin в f x на предобразе s.
LaTeX
$$$\\text{IsOpenEmbedding } f \\Rightarrow \\forall s:\\ Set β,\\\\forall x:\\ α, map f (\\mathcal{N}_{f^{-1}(s)}(x)) = \\mathcal{N}_{s}(f x)$$$
Lean4
theorem map_nhdsWithin_preimage_eq {f : α → β} (hf : IsOpenEmbedding f) (s : Set β) (x : α) :
map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x :=
by
rw [hf.isEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]
apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.isOpen_range
rw [inter_assoc, inter_self]