α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
⊢ IsOpen (PFun.preimage f Set.univ)
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
⊢ IsOpen (PFun.Dom f)
rw [← PFun.preimage_univ]
no goals
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α →. β
h : PContinuous f
⊢ IsOpen (PFun.preimage f Set.univ)
exact h _ isOpen_univ