∀ {α : Type u_2} (E : Type u_1) {m : MeasurableSpace α} [inst : NormedAddCommGroup E] (p : ENNReal)
  (μ : MeasureTheory.Measure α) {f g : α →ₘ[μ] E},
  f ∈ {f | MeasureTheory.eLpNorm (↑f) p μ < ⊤} →
    g ∈ {f | MeasureTheory.eLpNorm (↑f) p μ < ⊤} → f + g ∈ {f | MeasureTheory.eLpNorm (↑f) p μ < ⊤}