Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 09:27 ac006036

View on Github →

feat(measure_theory/measure/measure_space): add some null_measurable_set lemmas (#14293) Add measure_bUnion₀, measure_sUnion₀, and measure_bUnion_finset₀.

Estimated changes

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.lintegral_Union₀

added theorem measure_theory.lintegral_bUnion

added theorem measure_theory.lintegral_bUnion_finset

added theorem measure_theory.lintegral_bUnion_finset₀

added theorem measure_theory.lintegral_bUnion₀

Modified src/measure_theory/measure/ae_disjoint.lean

deleted theorem disjoint.ae_disjoint

Modified src/measure_theory/measure/measure_space.lean

modified theorem measure_theory.measure_bUnion_finset

added theorem measure_theory.measure_bUnion_finset₀

added theorem measure_theory.measure_bUnion₀

added theorem measure_theory.measure_sUnion₀