Currying smooth maps

Stream: Is there code for X?

[Oliver Nash]

Do we have anything along the following lines:

import measure_theory.function.lp_space

open measure_theory
open_locale ennreal

variables {E₁ E₂ F : Type*}
variables [normed_group E₁] [normed_space ℝ E₁]
variables [normed_group E₂] [normed_space ℝ E₂] [measure_space E₂] [borel_space E₂]
variables [normed_group F] [normed_space ℝ F]
variables {p : ℝ≥0∞} [fact (1 ≤ p)]

-- Is this true (maybe with finite-dimensionality, completeness, second-countability assumptions)?
lemma cont_diff_Lp_iff_cont_diff_curry {f : E₁ → Lp F p (@volume E₂ _)} :
  cont_diff ℝ ⊤ f ↔ cont_diff ℝ ⊤ (λ z : E₁ × E₂, f z.1 z.2) :=
sorry