Commit 2026-01-27 17:10 be615c75

View on Github →

feat(Asymptotics/TVS): prove that IsBigOTVS is equivalent to IsBigO (#34074)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/TVS.lean

added theorem Asymptotics.IsBigOTVS.of_egauge_le_mul

added theorem Asymptotics.isBigOTVS_iff_isBigO

modified theorem Asymptotics.isLittleOTVS_iff_isLittleO