Theorem MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral

Modification history

2025-11-21 04:24
Mathlib/MeasureTheory/Integral/Bochner/L1.lean
chore: make `CLM.extend` total and define `LM.leftInverse` (#31799) …
Added MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integralView on Github →