Def Filter.EventuallyConst

Modification history

2023-08-22 13:23

Mathlib/Order/Filter/EventuallyConst.lean

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

Modified Filter.EventuallyConst View on Github →

2023-06-19 16:31

Mathlib/Order/Filter/EventuallyConst.lean

feat: functions eventually constant along filters (#5248) …

Added Filter.EventuallyConst View on Github →