Commit 2023-06-27 20:47 1bd51828

View on Github →

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

Estimated changes

Modified Mathlib/Order/Filter/EventuallyConst.lean

added theorem Filter.EventuallyEq.eventuallyConst_iff