Theorem intervalIntegral.integral_congr_Ioo_of_le

Modification history

2026-06-22 10:16

Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

refactor(MeasureTheory/Measure/Typeclasses/NoAtoms): rename `NoAtoms` to `NullSingletonClass` (#40809) …

Modified intervalIntegral.integral_congr_Ioo_of_le View on Github →

2026-06-01 07:16

Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

feat(MeasureTheory/Integral): add integral_congr_uIoo (#39391) …

Added intervalIntegral.integral_congr_Ioo_of_le View on Github →