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