Theorem Filter.Tendsto.eventually_mem

Modification history

2024-10-21 09:29
Mathlib/Order/Filter/Basic.lean
chore(Filter/Tendsto): split from `Basic` (#17959)
Modified Filter.Tendsto.eventually_memView on Github →
2024-01-08 11:01
Mathlib/Order/Filter/Basic.lean
chore(Filter/AtTopBot): golf (#9521) …
Added Filter.Tendsto.eventually_memView on Github →