Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-03 06:55 cb0a1b50

View on Github →

feat(order/filter): add lemmas about ∀ᶠ, ∃ᶠ and logic operations (#2314)

feat(order/filter): add lemmas about ∀ᶠ, ∃ᶠ and logic operations
Remove @[congr]
Apply suggestions from code review Co-Authored-By: Gabriel Ebner gebner@gebner.org

Estimated changes

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.all_ae_and_iff

added theorem measure_theory.all_ae_imp_distrib_left

added theorem measure_theory.all_ae_or_distrib_left

added theorem measure_theory.all_ae_or_distrib_right

added theorem measure_theory.volume_zero_iff_all_ae_nmem

Modified src/order/filter/basic.lean

modified theorem filter.eventually.congr

deleted theorem filter.eventually.congr_iff

added theorem filter.eventually_and

added theorem filter.eventually_congr

added theorem filter.eventually_const

modified theorem filter.eventually_false_iff_eq_bot

added theorem filter.eventually_imp_distrib_left

added theorem filter.eventually_imp_distrib_right

added theorem filter.eventually_or_distrib_left

added theorem filter.eventually_or_distrib_right

modified theorem filter.frequently_bot

added theorem filter.frequently_const

modified theorem filter.frequently_false

added theorem filter.frequently_imp_distrib

added theorem filter.frequently_imp_distrib_left

added theorem filter.frequently_imp_distrib_right

added theorem filter.frequently_or_distrib

added theorem filter.frequently_or_distrib_left

added theorem filter.frequently_or_distrib_right

modified theorem filter.frequently_true_iff_ne_bot

Modified src/order/liminf_limsup.lean