no goals
α : Type u_1
β : Type u_2
γ : Type ?u.141298
δ : Type ?u.141301
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ f : α → β
h : ∀ (x : α), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f
x : α
g : β → α
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : Function.RightInverse g f
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))
rw [map_map, hgf.comp_eq_id, map_id]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.141298
δ : Type ?u.141301
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ f : α → β
h : ∀ (x : α), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f
x : α
g : β → α
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : Function.RightInverse g f
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)
rw [hgx]