case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous (Function.uncurry fun x y => ↑(uncurry x) y)
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous uncurry
apply continuous_of_continuous_uncurry
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous ((Function.uncurry fun x y => ↑(uncurry x) y) ∘ ↑(Homeomorph.prodAssoc C(α, C(β, γ)) α β))
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous (Function.uncurry fun x y => ↑(uncurry x) y)
rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
no goals
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous ((Function.uncurry fun x y => ↑(uncurry x) y) ∘ ↑(Homeomorph.prodAssoc C(α, C(β, γ)) α β))
apply continuous_eval'.comp (continuous_eval'.prod_map continuous_id)