Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-12 04:52 6fd688b5

View on Github →

chore(measure_theory): move mutually_singular to a new file (#10281)

Estimated changes

Modified src/measure_theory/integral/lebesgue.lean

Modified src/measure_theory/measure/measure_space.lean

deleted theorem measure_theory.measure.mutually_singular.add_left

deleted theorem measure_theory.measure.mutually_singular.add_left_iff

deleted theorem measure_theory.measure.mutually_singular.add_right

deleted theorem measure_theory.measure.mutually_singular.add_right_iff

deleted theorem measure_theory.measure.mutually_singular.comm

deleted theorem measure_theory.measure.mutually_singular.mk

deleted theorem measure_theory.measure.mutually_singular.mono

deleted theorem measure_theory.measure.mutually_singular.mono_ac

deleted theorem measure_theory.measure.mutually_singular.smul

deleted theorem measure_theory.measure.mutually_singular.smul_nnreal

deleted theorem measure_theory.measure.mutually_singular.sum_left

deleted theorem measure_theory.measure.mutually_singular.sum_right

deleted theorem measure_theory.measure.mutually_singular.symm

deleted theorem measure_theory.measure.mutually_singular.zero_left

deleted theorem measure_theory.measure.mutually_singular.zero_right

deleted def measure_theory.measure.mutually_singular

Created src/measure_theory/measure/mutually_singular.lean

added theorem measure_theory.measure.mutually_singular.add_left

added theorem measure_theory.measure.mutually_singular.add_left_iff

added theorem measure_theory.measure.mutually_singular.add_right

added theorem measure_theory.measure.mutually_singular.add_right_iff

added theorem measure_theory.measure.mutually_singular.comm

added theorem measure_theory.measure.mutually_singular.mk

added theorem measure_theory.measure.mutually_singular.mono

added theorem measure_theory.measure.mutually_singular.mono_ac

added theorem measure_theory.measure.mutually_singular.smul

added theorem measure_theory.measure.mutually_singular.smul_nnreal

added theorem measure_theory.measure.mutually_singular.sum_left

added theorem measure_theory.measure.mutually_singular.sum_right

added theorem measure_theory.measure.mutually_singular.symm

added theorem measure_theory.measure.mutually_singular.zero_left

added theorem measure_theory.measure.mutually_singular.zero_right

added def measure_theory.measure.mutually_singular