Theorem ContinuousAt.isLittleO

Modification history

2026-09-21 13:42
Mathlib/Analysis/Asymptotics/Lemmas.lean
feat(Analysis/Asymptotics): continuous / analytic functions are `IsTheta` at a point (#43810) …
Modified ContinuousAt.isLittleOView on Github →
2026-07-01 03:52
Mathlib/Analysis/Asymptotics/Lemmas.lean
feat(Analysis/Asymptotics): a function continuous at a point is bounded near it (#41201) …
Added ContinuousAt.isLittleOView on Github →