Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-14 08:04 2ceacc1a

View on Github →

feat(measure_theory/measure): more lemmas about null_measurable_sets (#12019)

Estimated changes

Modified src/measure_theory/group/fundamental_domain.lean

added theorem measure_theory.is_fundamental_domain.null_measurable_set_smul

Modified src/measure_theory/measure/measure_space.lean

modified theorem measure_theory.measure.restrict_Union_ae

added theorem measure_theory.measure.restrict_apply₀'

added theorem measure_theory.measure.restrict_restrict₀'

added theorem measure_theory.measure.restrict_restrict₀