Theorem Ergodic.ae_empty_or_univ_of_image_ae_le'

Modification history

2024-08-30 10:14

Mathlib/Dynamics/Ergodic/Ergodic.lean

chore(MeasureTheory): generalize to `NullMeasurableSet` (#16279) …

Modified Ergodic.ae_empty_or_univ_of_image_ae_le'View on Github →

2023-05-10 07:35

Mathlib/Dynamics/Ergodic/Ergodic.lean

feat: port Dynamics.Ergodic.Ergodic (#3879)

Added Ergodic.ae_empty_or_univ_of_image_ae_le'View on Github →