mathlib3

0817e7fe - feat(measure_theory): absolute continuity of the integral (#5743)

feat(measure_theory): absolute continuity of the integral (#5743) ### API changes: #### `ennreal`s and `nnreal`s: * `ennreal.mul_le_mul` and `ennreal.mul_lt_mul` are now `mono` lemmas; * rename `ennreal.sub_lt_sub_self` to `ennreal.sub_lt_self`: there is no `-` in the RHS; * new lemmas `enrneal.mul_div_le`, `nnreal.sub_add_eq_max`, and `nnreal.add_sub_eq_max`; * add new lemma `ennreal.bsupr_add`, use in in the proof of `ennreal.Sup_add`; #### Complete lattice * new lemma `supr_lt_iff`; #### Simple functions * new lemmas `simple_func.exists_forall_le`, `simple_func.map_add`, `simple_func.sub_apply`; * weaker typeclass assumptions in `simple_func.coe_sub`; * `monotone_eapprox` is now a `mono` lemma; #### Integration * new lemmas `exists_simple_func_forall_lintegral_sub_lt_of_pos`, `exists_pos_set_lintegral_lt_of_measure_lt`, `tendsto_set_lintegral_zero`, and `has_finite_integral.tendsto_set_integral_nhds_zero`.