Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-07 10:12 ae98aad6

View on Github →

chore(measure_theory/measure): review API of mutually_singular (#10186)

Estimated changes

Modified src/measure_theory/decomposition/jordan.lean

Modified src/measure_theory/decomposition/lebesgue.lean

deleted def measure_theory.signed_measure.singular_part(s

added def measure_theory.signed_measure.singular_part

Modified src/measure_theory/integral/lebesgue.lean

Modified src/measure_theory/measure/measure_space.lean

deleted theorem measure_theory.measure.mutually_singular.add

deleted theorem measure_theory.measure.mutually_singular.add_iff

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

deleted theorem measure_theory.measure.mutually_singular.of_absolutely_continuous

modified 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

modified theorem measure_theory.measure.mutually_singular.symm

modified theorem measure_theory.measure.mutually_singular.zero_left

modified theorem measure_theory.measure.mutually_singular.zero_right

added theorem measure_theory.measure.sum_of_empty

Modified src/topology/instances/ennreal.lean