Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-09 19:22 40b55c0b

View on Github →

feat(measure_theory): additions (#4324) Many additional lemmas. Notable addition: sequential limits of measurable functions into a metric space are measurable. Rename integral_map_measure -> integral_map (to be consistent with the version for lintegral) Fix the precedence of all notations for integrals. From now on ∫ x, abs ∥f x∥ ∂μ will be parsed correctly (previously it gave a parse error). Some cleanup (moving lemmas, and some nicer presentation by opening locales and namespaces).

Estimated changes

added theorem set.indicator_prod_one
added theorem set.Union_Inter_subset
added theorem set.Union_inter_subset
added theorem ite_and
modified theorem ennreal.measurable_coe
modified theorem measurable.ennreal_coe
added theorem measurable.inf_nndist
modified theorem measurable.nnnorm
modified theorem measurable.nnreal_coe
modified theorem measurable.norm
modified theorem measurable.sub_nnreal
modified theorem measurable_dist
modified theorem measurable_edist
modified theorem measurable_ennreal_coe_iff
added theorem measurable_inf_nndist
added theorem measurable_liminf'
added theorem measurable_liminf
added theorem measurable_limsup'
added theorem measurable_limsup
modified theorem measurable_nndist
modified theorem measurable_nnnorm
modified theorem nnreal.measurable_coe
modified theorem measure_theory.dirac_ae_eq
added theorem integral_smul_const