English
If f is left-inverse to g on a domain and certain continuity conditions hold at x, then map g (nhds x) equals nhds at g x restricted to range, i.e., map g (nhds x) = nhdsWithin (g x) (range g).
Русский
Если f является левым обратным к g на области и соблюдены условия непрерывности в точке x, то map g (nhds x) = nhdsWithin (g x) (range g).
LaTeX
$$$\\text{LeftInverse } f\\ g \\Rightarrow \\text{map } g (\\mathcal{N} x) = \\mathcal{N}_{\\mathrm{range} g}(g x)$ under hypotheses$$
Lean4
theorem map_nhds_eq {f : α → β} {g : β → α} {x : β} (h : Function.LeftInverse f g)
(hf : ContinuousWithinAt f (range g) (g x)) (hg : ContinuousAt g x) : map g (𝓝 x) = 𝓝[range g] g x := by
simpa only [nhdsWithin_univ, image_univ] using
(h.leftInvOn univ).map_nhdsWithin_eq (h x) (by rwa [image_univ]) hg.continuousWithinAt
