α : Type u_1
β : Type u_2
γ : Type ?u.139510
δ : Type ?u.139513
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
⊢ IsOpen (f '' univ)
α : Type u_1
β : Type u_2
γ : Type ?u.139510
δ : Type ?u.139513
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
⊢ IsOpen (range f)
rw [← image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.139510
δ : Type ?u.139513
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
⊢ IsOpen (f '' univ)
exact hf _ isOpen_univ