Theorem Filter.eventuallyConst_iff_exists_eventuallyEq

Modification history

2023-08-22 13:23
Mathlib/Order/Filter/EventuallyConst.lean
refactor(Filter/EventuallyConst): redefine (#6673)
Added Filter.eventuallyConst_iff_exists_eventuallyEqView on Github →