Theorem Filter.Tendsto.sup_sup

Modification history

2024-10-21 09:29
Mathlib/Order/Filter/Basic.lean
chore(Filter/Tendsto): split from `Basic` (#17959)
Modified Filter.Tendsto.sup_supView on Github →
2024-04-21 06:33
Mathlib/Order/Filter/Basic.lean
feat: tendsto on a supremum (#12308)
Added Filter.Tendsto.sup_supView on Github →