Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-03 17:56 6993e6f8

View on Github →

feat(measure_theory/constructions/borel_space): decomposing the measure of a set into slices (#10096) Also add the fact that μ (to_measurable μ t ∩ s) = μ (t ∩ s), and useful variations around this fact.

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

added theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow

Modified src/measure_theory/measure/finite_measure_weak_convergence.lean

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.measure.coe_nnreal_smul_apply

added theorem measure_theory.measure.measure_eq_left_of_subset_of_measure_add_eq

added theorem measure_theory.measure.measure_eq_right_of_subset_of_measure_add_eq

added theorem measure_theory.measure.measure_inter_eq_of_measure_eq

added theorem measure_theory.measure.measure_to_measurable_add_inter_left

added theorem measure_theory.measure.measure_to_measurable_add_inter_right

added theorem measure_theory.measure.measure_to_measurable_inter

modified theorem measure_theory.measure.smul_apply

Modified src/measure_theory/measure/measure_space_def.lean

Modified src/measure_theory/measure/regular.lean

added theorem set.exists_is_open_le_add