Commit 2023-05-10 00:18 672941e4

View on Github →

feat: port MeasureTheory.Measure.MutuallySingular (#3818)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/MutuallySingular.lean

added theorem MeasureTheory.Measure.MutuallySingular.add_left

added theorem MeasureTheory.Measure.MutuallySingular.add_left_iff

added theorem MeasureTheory.Measure.MutuallySingular.add_right

added theorem MeasureTheory.Measure.MutuallySingular.add_right_iff

added theorem MeasureTheory.Measure.MutuallySingular.comm

added theorem MeasureTheory.Measure.MutuallySingular.mk

added theorem MeasureTheory.Measure.MutuallySingular.mono

added theorem MeasureTheory.Measure.MutuallySingular.mono_ac

added theorem MeasureTheory.Measure.MutuallySingular.smul

added theorem MeasureTheory.Measure.MutuallySingular.smul_nnreal

added theorem MeasureTheory.Measure.MutuallySingular.sum_left

added theorem MeasureTheory.Measure.MutuallySingular.sum_right

added theorem MeasureTheory.Measure.MutuallySingular.symm

added theorem MeasureTheory.Measure.MutuallySingular.zero_left

added theorem MeasureTheory.Measure.MutuallySingular.zero_right

added def MeasureTheory.Measure.MutuallySingular