Commit 2024-02-22 06:08 a319cfe8
View on Github →feat: Add ContinuousAt.eventually_mem (#10838)
This is essentially the same as Filter.Tendsto.eventually_mem, but infers in more cases when applied.
Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ContinuousAt.2Eeventually_mem'/near/422664457