theorem
MemLp.toLp_sum
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_3}
[DecidableEq ι]
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ i ∈ s, MeasureTheory.MemLp (f i) p μ)
: