Theorem Filter.eventuallyConst_iff_tendsto

Modification history

2023-08-22 13:23
Mathlib/Order/Filter/EventuallyConst.lean
refactor(Filter/EventuallyConst): redefine (#6673)
Modified Filter.eventuallyConst_iff_tendstoView on Github →
2023-06-19 16:31
Mathlib/Order/Filter/EventuallyConst.lean
feat: functions eventually constant along filters (#5248) …
Added Filter.eventuallyConst_iff_tendstoView on Github →