Mathlib Changelog
v4
Changelog
About
Github
Theorem
tendsto_atBot_of_monotone
Modification history
2026-01-26 12:23
Mathlib/Topology/Order/MonotoneConvergence.lean
chore: add `atBot` version of convergence lemmas, rename original lemma for disambiguation (#34413) …
Added
tendsto_atBot_of_monotone
View on Github →