Theorem DifferentiableWithinAt.isBigO_sub

Modification history

2026-02-05 07:38
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
chore(Calculus/FDeriv): review asymptotics lemmas (#34832) …
Modified DifferentiableWithinAt.isBigO_subView on Github →
2023-11-12 09:05
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
feat(Calculus/FDeriv): add `DifferentiableAt.isBigO_sub` (#8352) …
Added DifferentiableWithinAt.isBigO_subView on Github →