∀ {α : Type u_1} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε],
  q ≠ 0 → μ ≠ 0 → ∀ {f : α → ε}, f =ᵐ[μ] 0 → MeasureTheory.eLpNorm' f q μ = 0