mathlib
e99ff889 - feat(measure_theory): add `restrict_inter_add_diff` and `lintegral_inter_add_diff` (#14280)

Commit
3 years ago
feat(measure_theory): add `restrict_inter_add_diff` and `lintegral_inter_add_diff` (#14280) * add `measure_theory.measure.restrict_inter_add_diff` and `measure_theory.lintegral_inter_add_diff`; * drop one measurability assumption in `measure_theory.lintegral_union`; * add `measure_theory.lintegral_max` and `measure_theory.set_lintegral_max`; * drop `measure_theory.measure.lebesgue_decomposition.max_measurable_le`: use `set_lintegral_max` instead.
Author
Parents
Loading