Theorem intervalIntegral.integral_Ici_sub_Ici'

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_Ici_sub_Ici'View on Github →

2026-04-24 08:11

Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

feat(MeasureTheory): Integral over Ioi tends to zero (#34298) …

Added intervalIntegral.integral_Ici_sub_Ici'View on Github →