Commit 2022-02-12 22:55 af1355c4

View on Github →

chore(measure_theory/integral/lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000) I also grouped similar lemmas together and added one or two missing ones.

Estimated changes

Modified src/measure_theory/integral/lebesgue.lean

deleted theorem measure_theory.simple_func.add_apply

deleted theorem measure_theory.simple_func.add_eq_map₂

deleted theorem measure_theory.simple_func.coe_add

added theorem measure_theory.simple_func.coe_div

added theorem measure_theory.simple_func.coe_inv

modified theorem measure_theory.simple_func.coe_mul

deleted theorem measure_theory.simple_func.coe_neg

added theorem measure_theory.simple_func.coe_one

deleted theorem measure_theory.simple_func.coe_sub

deleted theorem measure_theory.simple_func.coe_zero

added theorem measure_theory.simple_func.const_one

deleted theorem measure_theory.simple_func.const_zero

added theorem measure_theory.simple_func.div_apply

added theorem measure_theory.simple_func.inf_apply

added theorem measure_theory.simple_func.inv_apply

deleted theorem measure_theory.simple_func.map_add

added theorem measure_theory.simple_func.map_mul

modified theorem measure_theory.simple_func.mul_apply

modified theorem measure_theory.simple_func.mul_eq_map₂

added theorem measure_theory.simple_func.range_one

deleted theorem measure_theory.simple_func.range_zero

deleted theorem measure_theory.simple_func.sub_apply

modified theorem measure_theory.simple_func.sup_eq_map₂