Theorem MeasureTheory.lintegral_indicator_const₀

Modification history

2023-08-13 09:51
Mathlib/MeasureTheory/Integral/Lebesgue.lean
chore(LpSpace): golf, generalize (#6553) …
Added MeasureTheory.lintegral_indicator_const₀View on Github →