Commit 2023-08-01 18:35 ac5134b0

View on Github →

feat: add MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le (#6175) Also some minor loosely-related other changes.

Estimated changes

Modified Mathlib/Algebra/Ring/BooleanRing.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Pointwise.lean

added theorem Finset.smul_finset_symmDiff₀

deleted theorem Finset.smul_finset_symm_diff₀

Modified Mathlib/Data/Real/ENNReal.lean

added theorem ENNReal.abs_toReal

added theorem ENNReal.toReal_nsmul

Modified Mathlib/Data/Set/Image.lean

added theorem Set.image_symmDiff

deleted theorem Set.image_symm_diff

added theorem Set.preimage_symmDiff

added theorem Set.subset_image_symmDiff

deleted theorem Set.subset_image_symm_diff

Modified Mathlib/Data/Set/Pointwise/SMul.lean

added theorem Set.smul_set_symmDiff

added theorem Set.smul_set_symmDiff₀

deleted theorem Set.smul_set_symm_diff

deleted theorem Set.smul_set_symm_diff₀

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

added theorem MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff'

added theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff

added theorem MeasureTheory.measure_symmDiff_eq

added theorem MeasureTheory.measure_symmDiff_le

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem MeasureTheory.measure_le_measure_union_left

added theorem MeasureTheory.measure_le_measure_union_right

added theorem MeasureTheory.measure_lt_top_of_subset

Modified Mathlib/Order/Hom/Lattice.lean

added theorem map_symmDiff'

deleted theorem map_symm_diff'