Theorem Filter.EventuallyEq.eventuallyConst_iff

Modification history

2023-08-22 13:23

Mathlib/Order/Filter/EventuallyConst.lean

refactor(Filter/EventuallyConst): redefine (#6673)

Modified Filter.EventuallyEq.eventuallyConst_iff View on Github →

2023-06-27 20:47

Mathlib/Order/Filter/EventuallyConst.lean

feat: add `Filter.EventuallyConst.congr` and `Filter.EventuallyEq.eventuallyConst_iff` (#5433)

Added Filter.EventuallyEq.eventuallyConst_iff View on Github →