Theorem ContinuousAt.isBigO

Modification history

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.isBigOView on Github →