Theorem Filter.eventually_imp_distrib_left

Modification history

2024-11-29 19:27
Mathlib/Order/Filter/Basic.lean
chore(Filter/Prod): drop `Filter.prod`, use `SProd` instead (#18315) …
Modified Filter.eventually_imp_distrib_leftView on Github →
2024-11-25 09:04
Mathlib/Order/Filter/Basic.lean
chore: split Order.Filter.Basic, creating Order.Filter.Finite (#19354)
Modified Filter.eventually_imp_distrib_leftView on Github →
2023-01-23 08:16
Mathlib/Order/Filter/Basic.lean
Feat: port Order.Filter.Basic (#1750)
Added Filter.eventually_imp_distrib_leftView on Github →