Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-26 18:24 a491055c

View on Github →

chore(measure_theory/integral/lebesgue): extend to ae_measurable (#12953)

Estimated changes

Modified src/measure_theory/group/arithmetic.lean

Modified src/measure_theory/integral/lebesgue.lean

modified theorem measure_theory.lintegral_eq_top_of_measure_eq_top_pos

modified theorem measure_theory.lintegral_trim

modified theorem measure_theory.meas_ge_le_lintegral_div

added theorem measure_theory.mul_meas_ge_le_lintegral₀

added theorem measure_theory.simple_func.apply_mk

added theorem measure_theory.simple_func.extend_apply'

added def measure_theory.simple_func.of_is_empty

modified theorem measure_theory.univ_le_of_forall_fin_meas_le