Theorem Filter.eventually_sub_nonneg

Modification history

2025-04-10 16:38
Mathlib/Order/Filter/Ring.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified Filter.eventually_sub_nonnegView on Github →
2025-03-19 06:49
Mathlib/Order/Filter/Ring.lean
feat: generalize Mathlib.Order (#23062) …
Modified Filter.eventually_sub_nonnegView on Github →
2024-06-27 21:04
Mathlib/Order/Filter/Basic.lean
chore(Order/Filter/Basic): assert_not_exists OrderedSemiring (#14179)
Modified Filter.eventually_sub_nonnegView on Github →
2023-01-23 08:16
Mathlib/Order/Filter/Basic.lean
Feat: port Order.Filter.Basic (#1750)
Added Filter.eventually_sub_nonnegView on Github →