∀ {α : Type u_1} (𝕜 : Type u_3) {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (p : ENNReal)
  {q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] (f : ↥(MeasureTheory.Lp E q μ)), 0 • f = 0