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