no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.103929
α : Type ?u.103932
ι : Type ?u.103935
π : ι → Type ?u.103940
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
s : Set (SeparationQuotient X)
⊢ ContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s)
simp only [ContinuousOn, surjective_mk.forall, continuousWithinAt_lift, mem_preimage]