mathlib
3cfaa0bf - feat(measure_theory/measure_space): add ae_imp_iff (#6218)

Commit

4 years ago

feat(measure_theory/measure_space): add ae_imp_iff (#6218) This is `filter.eventually_imp_distrib_left` specialized to the measure.ae filter.

Author

RemyDegenne

Parents