MeasureTheory.support_sigma_finite_from_MemLp

lemma support_sigma_finite_from_MemLp    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    (hf : MemLp f p μ) (hp : p ≠ ⊤) (hp' : p ≠ 0) :    SigmaFinite (μ.restrict (fun x ↦ ‖f x‖ₑ).support) := by  let g : α → ℝ≥0∞ := fun x ↦ ‖f x‖ₑ ^ p.toReal  have : g.support = (fun x ↦ ‖f x‖ₑ).support := by    unfold Function.support g    ext x    simp only [ne_eq, ENNReal.rpow_eq_zero_iff, not_or, not_and, not_lt,      toReal_nonneg, implies_true, and_true, mem_setOf_eq]    constructor    · contrapose      simp [Classical.not_imp, not_le, toReal_pos hp' hp]    · intro h h'      contradiction  rw [← this]  apply support_sigma_finite_of_lintegrable  · exact hf.1.enorm.pow_const _  · unfold g    have obs := hf.2    unfold eLpNorm eLpNorm' at obs    split_ifs at obs    · contradiction    · exact lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top (toReal_pos hp' hp) obs