Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-16 12:14 809e920e

View on Github →

feat(dynamics/ergodic/ergodic): expand ergodic map API for finite measures (#17864)

Estimated changes

Modified src/dynamics/ergodic/ergodic.lean

added theorem ergodic.ae_empty_or_univ_of_ae_le_preimage'

added theorem ergodic.ae_empty_or_univ_of_ae_le_preimage

added theorem ergodic.ae_empty_or_univ_of_image_ae_le'

added theorem ergodic.ae_empty_or_univ_of_image_ae_le

added theorem ergodic.ae_empty_or_univ_of_preimage_ae_le'

added theorem ergodic.ae_empty_or_univ_of_preimage_ae_le

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.ae_eq_of_ae_subset_of_measure_ge

added theorem measure_theory.union_ae_eq_left_iff_ae_subset

added theorem measure_theory.union_ae_eq_right_iff_ae_subset

Modified src/measure_theory/measure/measure_space_def.lean

added theorem measure_theory.ae_le_set_union

modified theorem measure_theory.union_ae_eq_right