English
If f and g satisfy a left-inverse relation on s (LeftInvOn f g s), and x ∈ domain with appropriate continuity hypotheses, then the pushforward of nhdsWithin by g equals the nhdsWithin at g x on the image, i.e., map g (𝓝[s] x) = 𝓝[g''s] g x.
Русский
Если f и g удовлетворяют отношению левого обратного на s (LeftInvOn f g s), и выполняются соответствующие условия непрерывности, то образ nhdsWithin через g равен nhdsWithin в g x на образе: map g (𝓝[s] x) = 𝓝[g '' s] g x.
LaTeX
$$$\\text{LeftInvOn } f\\ g\\ s \\Rightarrow \\text{map } g (\\mathcal{N}_{s}(x)) = \\mathcal{N}_{g''s}(g x)$ under appropriate hypotheses$$
Lean4
theorem map_nhdsWithin_eq {f : α → β} {g : β → α} {x : β} {s : Set β} (h : LeftInvOn f g s) (hx : f (g x) = x)
(hf : ContinuousWithinAt f (g '' s) (g x)) (hg : ContinuousWithinAt g s x) : map g (𝓝[s] x) = 𝓝[g '' s] g x :=
by
apply le_antisymm
· exact hg.tendsto_nhdsWithin (mapsTo_image _ _)
· have A : g ∘ f =ᶠ[𝓝[g '' s] g x] id := h.rightInvOn_image.eqOn.eventuallyEq_of_mem self_mem_nhdsWithin
refine le_map_of_right_inverse A ?_
simpa only [hx] using hf.tendsto_nhdsWithin (h.mapsTo (surjOn_image _ _))
