Commit 2025-03-21 07:31 90d9a017

View on Github →

feat(Analysis/Asymptotics) IsBigO.add_iff_left and variants (#23059) Add bidirectional variants of IsBigO.sub and IsBigO.add.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Defs.lean

added theorem Asymptotics.IsBigO.add_iff_left

added theorem Asymptotics.IsBigO.add_iff_right

added theorem Asymptotics.IsBigO.sub_iff_left

added theorem Asymptotics.IsBigO.sub_iff_right

added theorem Asymptotics.IsLittleO.add_iff_left

added theorem Asymptotics.IsLittleO.add_iff_right

added theorem Asymptotics.IsLittleO.sub_iff_left

added theorem Asymptotics.IsLittleO.sub_iff_right