Theorem Filter.EventuallyEq.comp_tendsto

Modification history

2024-10-21 09:29
Mathlib/Order/Filter/Basic.lean
chore(Filter/Tendsto): split from `Basic` (#17959)
Modified Filter.EventuallyEq.comp_tendstoView on Github →
2024-07-01 17:37
Mathlib/Order/Filter/Basic.lean
chore(Order): remove almost all autoImplicit (#14304) …
Modified Filter.EventuallyEq.comp_tendstoView on Github →
2024-02-26 23:59
Mathlib/Order/Filter/Basic.lean
feat: lemmas about germs in topological spaces (#9747) …
Modified Filter.EventuallyEq.comp_tendstoView on Github →
2023-02-15 08:14
Mathlib/Order/Filter/Germ.lean
feat: port Order.Filter.Germ (#1799)
Added Filter.EventuallyEq.comp_tendstoView on Github →