Theorem Asymptotics.IsLittleO.add_iff_left

Modification history

2025-03-21 07:31
Mathlib/Analysis/Asymptotics/Defs.lean
feat(Analysis/Asymptotics) `IsBigO.add_iff_left` and variants (#23059) …
Added Asymptotics.IsLittleO.add_iff_leftView on Github →