no goals
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type ?u.113085
ι : Type ?u.113088
π : ι → Type ?u.113093
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 → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
⊢ Continuous (uncurry (lift₂ f hf)) ↔ Continuous (uncurry f)
simp only [continuous_iff_continuousOn_univ, continuousOn_lift₂, preimage_univ]