Theorem MeasureTheory.integral_indicatorConstLp

Modification history

2023-07-17 03:51

Mathlib/MeasureTheory/Integral/SetIntegral.lean

feat(MeasureTheory.Integral.Bochner): drop completeness requirement from the definition (#5910) …

Modified MeasureTheory.integral_indicatorConstLp View on Github →

2023-06-06 00:38

Mathlib/MeasureTheory/Integral/SetIntegral.lean

feat: port MeasureTheory.Integral.SetIntegral (#4690)

Added MeasureTheory.integral_indicatorConstLp View on Github →