Commit 2023-06-29 08:26 3ae1d053
View on Github →feat: add PreErgodic.ae_mem_or_ae_nmem etc (#5220)
Add versions of some of the PreErgodic.ae_empty_or_univ etc lemmas
in terms of (∀ᵐ x ∂μ, x ∈ s) ∨ (∀ᵐ x ∂μ, x ∉ s) instead of
a.e. equality of sets.