Commit 2021-01-08 02:05 4c3c8d78

View on Github →

feat(measure_theory): some additions (#5653) rename exists_is_measurable_superset_of_measure_eq_zero -> exists_is_measurable_superset_of_null make measure.prod and measure.pi irreducible

Estimated changes

Modified src/measure_theory/borel_space.lean

added theorem ennreal.measurable_div

added theorem ennreal.measurable_inv

modified def homeomorph.to_measurable_equiv

added theorem homeomorph.to_measurable_equiv_coe

added theorem homeomorph.to_measurable_equiv_symm_coe

added theorem measurable.ennreal_div

added theorem measurable.ennreal_inv

Modified src/measure_theory/integration.lean

added theorem measure_theory.lintegral_lintegral_mul

added theorem measure_theory.lintegral_one

added theorem measure_theory.set_lintegral_const

Modified src/measure_theory/measurable_space.lean

added theorem measurable_equiv.self_comp_symm

added theorem measurable_equiv.symm_comp_self

Modified src/measure_theory/measure_space.lean

deleted theorem measure_theory.exists_is_measurable_superset_of_measure_eq_zero

added theorem measure_theory.exists_is_measurable_superset_of_null

Modified src/measure_theory/pi.lean

Modified src/measure_theory/prod.lean

added theorem measure_theory.lintegral_prod_mul