Theorem Asymptotics.isBigOTVS_iff_isBigO

Modification history

2026-01-27 17:10
Mathlib/Analysis/Asymptotics/TVS.lean
feat(Asymptotics/TVS): prove that `IsBigOTVS` is equivalent to `IsBigO` (#34074)
Added Asymptotics.isBigOTVS_iff_isBigOView on Github →