Theorem MeasureTheory.nontrivial_Lp_real_of_nontrivial_Lp

Modification history

2026-05-26 05:08
Mathlib/MeasureTheory/Function/LpSpace/CompleteOfCompleteLp.lean
feat: if an L^p space is complete, so is its target space unless the measure is zero (#39614)
Added MeasureTheory.nontrivial_Lp_real_of_nontrivial_LpView on Github →