Commit 2023-11-01 08:43 d3e3459d

View on Github →

feat: restriction to {a}ᶜ is equal to the original measure (#8073) Also reuse variables from variable here and there.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem Finset.measure_zero

added theorem MeasureTheory.restrict_compl_singleton

modified theorem Set.Countable.ae_not_mem

added theorem Set.Countable.measure_restrict_compl

modified theorem Set.Countable.measure_zero

modified theorem Set.Finite.measure_zero

modified theorem Set.Subsingleton.measure_zero