no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.105005
α : Type ?u.105008
ι : Type ?u.105011
π : ι → Type ?u.105016
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
⊢ Continuous (lift f hf) ↔ Continuous f
simp only [continuous_iff_continuousOn_univ, continuousOn_lift, preimage_univ]