Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-02 05:25 8ef783b4

View on Github →

feat(measure_theory/measure): drop more measurable_set args (#11547) Most notably, in measure_Union_eq_supr.

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

deleted theorem bsupr_measure_Iic

Modified src/measure_theory/decomposition/unsigned_hahn.lean

Modified src/measure_theory/integral/lebesgue.lean

Modified src/measure_theory/integral/set_integral.lean

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.ae_eq_of_subset_of_measure_ge

added theorem measure_theory.bsupr_measure_Iic

modified theorem measure_theory.measure.ext_iff_of_Union_eq_univ

modified theorem measure_theory.measure.ext_iff_of_sUnion_eq_univ

modified theorem measure_theory.measure.restrict_Union_congr

modified theorem measure_theory.measure.restrict_bUnion_congr

modified theorem measure_theory.measure.restrict_finset_bUnion_congr

modified theorem measure_theory.measure.restrict_sUnion_congr

modified theorem measure_theory.measure.restrict_union_congr

added theorem measure_theory.measure_Union_congr_of_subset

modified theorem measure_theory.measure_Union_eq_supr

added theorem measure_theory.measure_Union_to_measurable

added theorem measure_theory.measure_add_diff

added theorem measure_theory.measure_bUnion_to_measurable

added theorem measure_theory.measure_diff'

added theorem measure_theory.measure_to_measurable_union

added theorem measure_theory.measure_union_congr_of_subset

added theorem measure_theory.measure_union_to_measurable

modified theorem measure_theory.tendsto_measure_Union

Modified src/measure_theory/measure/measure_space_def.lean

added theorem measure_theory.exists_measurable_superset₂

Modified src/measure_theory/measure/regular.lean

modified theorem measure_theory.measure.inner_regular.is_compact_is_closed

modified theorem measure_theory.measure.inner_regular.of_pseudo_emetric_space

Modified src/topology/metric_space/hausdorff_distance.lean