Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-10 07:18 ae86776f

View on Github →

feat(measure_theory/measure/vector_measure): define mutually singular for vector measures (#8896)

Estimated changes

Modified src/measure_theory/decomposition/jordan.lean

added theorem measure_theory.signed_measure.absolutely_continuous_ennreal_iff

deleted theorem measure_theory.signed_measure.absolutely_continuous_iff

added theorem measure_theory.signed_measure.mutually_singular_ennreal_iff

added theorem measure_theory.signed_measure.mutually_singular_iff

added theorem measure_theory.signed_measure.null_of_total_variation_zero

Modified src/measure_theory/measure/vector_measure.lean

added theorem measure_theory.vector_measure.mutually_singular.add_left

added theorem measure_theory.vector_measure.mutually_singular.add_right

added theorem measure_theory.vector_measure.mutually_singular.mk

added theorem measure_theory.vector_measure.mutually_singular.smul_left

added theorem measure_theory.vector_measure.mutually_singular.smul_right

added theorem measure_theory.vector_measure.mutually_singular.symm

added theorem measure_theory.vector_measure.mutually_singular.zero_left

added theorem measure_theory.vector_measure.mutually_singular.zero_right

added def measure_theory.vector_measure.mutually_singular