Theorem MeasureTheory.Integrable.add''

Modification history

2025-05-13 15:31

Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

feat(L1Space/Integrable): generalise to enorms (#24820) …

Modified MeasureTheory.Integrable.add''View on Github →

2025-01-22 16:34

Mathlib/MeasureTheory/Function/L1Space.lean

feat: make `Integrable` provable by `fun_prop` (#20952)

Added MeasureTheory.Integrable.add''View on Github →