α : Type u_1
β : Type u_2
γ : Type ?u.329904
δ : Type ?u.329907
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (f '' univ)
α : Type u_1
β : Type u_2
γ : Type ?u.329904
δ : Type ?u.329907
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (range f)
rw [← image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.329904
δ : Type ?u.329907
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (f '' univ)
exact (hf.restrict isOpen_univ).continuousOn_image_of_leftInvOn fun x _ => hleft x