Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-11 13:22 270c644c

View on Github →

feat(measure_theory): add ae_measurable.sum_measure (#10271) Also add a few supporting lemmas.

Estimated changes

Modified src/measure_theory/measurable_space.lean

added theorem measurable_of_subsingleton_codomain

Modified src/measure_theory/measure/measure_space.lean

added theorem ae_measurable.sum_measure

added theorem ae_measurable_Union_iff

modified theorem ae_measurable_add_measure_iff

added theorem ae_measurable_of_subsingleton_codomain

added theorem ae_measurable_sum_measure_iff

added theorem measure_theory.measure.ae_sum_eq

added theorem measure_theory.measure.ae_sum_iff'

added theorem measure_theory.measure.ae_sum_iff

added theorem measure_theory.measure.restrict_Union_ae

added theorem measure_theory.measure.restrict_Union_apply_ae

added theorem measure_theory.measure.sum_apply_eq_zero'

added theorem measure_theory.measure.sum_apply_eq_zero