Theorem QuasiErgodic.ae_empty_or_univ₀

Modification history

2023-06-29 08:26
Mathlib/Dynamics/Ergodic/Ergodic.lean
feat: add `PreErgodic.ae_mem_or_ae_nmem` etc (#5220) …
Added QuasiErgodic.ae_empty_or_univ₀View on Github →