Commit 2025-11-24 15:41 c887d0bf

View on Github →

feat(MeasureSpace): add cofinite_le_ae (#31962) Also add cofinite_eq_bot

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.cofinite_le_ae

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean

added theorem MeasureTheory.cofinite_eq_bot

added theorem MeasureTheory.cofinite_eq_bot_iff