Commit 2026-07-01 03:52 9ae96ab9

feat(Analysis/Asymptotics): a function continuous at a point is bounded near it (#41201) Add ContinuousAt.isBigO: if f is continuous at x then f =O[𝓝 x] (fun _ ↦ 1). This is a corollary of continuousAt_iff_isLittleO and has been placed accordingly.