Theorem integral_of_real

Modification history

2023-06-07 06:21

Mathlib/MeasureTheory/Integral/SetIntegral.lean

feat: port MeasureTheory.Integral.IntervalIntegral (#4710)

Deleted integral_of_real View on Github →

2023-06-06 00:38

Mathlib/MeasureTheory/Integral/SetIntegral.lean

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

Added integral_of_real View on Github →