Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-11-28 16:50
10a37a90
View on Github →
feat(MeasureTheory/Measure/MutuallySingular): Disjoint iff mutually singular (
#17995
)
Estimated changes
Modified
Mathlib/Analysis/SpecificLimits/Basic.lean
added
theorem
ENNReal.eq_zero_of_le_mul_pow
Modified
Mathlib/MeasureTheory/Measure/MeasureSpace.lean
added
theorem
MeasureTheory.Measure.inf_apply
Modified
Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
Modified
Mathlib/MeasureTheory/Measure/MutuallySingular.lean
added
theorem
MeasureTheory.Measure.MutuallySingular.disjoint
added
theorem
MeasureTheory.Measure.MutuallySingular.disjoint_ae
added
theorem
MeasureTheory.Measure.disjoint_of_disjoint_ae
added
theorem
MeasureTheory.Measure.exists_null_set_measure_lt_of_disjoint
added
theorem
MeasureTheory.Measure.mutuallySingular_iff_disjoint
added
theorem
MeasureTheory.Measure.mutuallySingular_iff_disjoint_ae
added
theorem
MeasureTheory.Measure.mutuallySingular_of_disjoint
added
theorem
MeasureTheory.Measure.mutuallySingular_tfae