Commit 2021-12-09 14:52 9ef122d2

View on Github →

feat(measure_theory/integral/set_to_l1): properties of (dominated_)fin_meas_additive (#10590) Various properties of fin_meas_additive and dominated_fin_meas_additive which will be useful to generalize results about integrals to set_to_fun.

Estimated changes

Modified src/measure_theory/integral/set_to_l1.lean

added theorem measure_theory.dominated_fin_meas_additive.add

added theorem measure_theory.dominated_fin_meas_additive.add_measure_left

added theorem measure_theory.dominated_fin_meas_additive.add_measure_right

added theorem measure_theory.dominated_fin_meas_additive.eq_zero

added theorem measure_theory.dominated_fin_meas_additive.eq_zero_of_measure_zero

added theorem measure_theory.dominated_fin_meas_additive.of_measure_le

added theorem measure_theory.dominated_fin_meas_additive.of_measure_le_smul

added theorem measure_theory.dominated_fin_meas_additive.of_smul_measure

added theorem measure_theory.dominated_fin_meas_additive.smul

added theorem measure_theory.dominated_fin_meas_additive.zero

modified def measure_theory.dominated_fin_meas_additive

added theorem measure_theory.fin_meas_additive.add

added theorem measure_theory.fin_meas_additive.map_Union_fin_meas_set_eq_sum

added theorem measure_theory.fin_meas_additive.map_empty_eq_zero

added theorem measure_theory.fin_meas_additive.of_eq_top_imp_eq_top

added theorem measure_theory.fin_meas_additive.of_smul_measure

added theorem measure_theory.fin_meas_additive.smul

added theorem measure_theory.fin_meas_additive.smul_measure

added theorem measure_theory.fin_meas_additive.smul_measure_iff

added theorem measure_theory.fin_meas_additive.zero

deleted theorem measure_theory.map_Union_fin_meas_set_eq_sum

deleted theorem measure_theory.map_empty_eq_zero_of_map_union