no goals
α : Type u_2
β : Type u_1
γ : Type ?u.339400
δ : Type ?u.339403
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ map g (𝓝 x) = 𝓝[range g] g x
simpa only [nhdsWithin_univ, image_univ] using
  (h.leftInvOn univ).map_nhdsWithin_eq (h x) (by rwa [image_univ]) hg.continuousWithinAt
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.339400
δ : Type ?u.339403
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ ContinuousWithinAt f (g '' univ) (g x)
rwa [image_univ]