Commit 2026-02-03 22:04 b8498633

View on Github →

feat(Asymptotics/TVS): fix a name, add isThetaTVS_iff_isTheta (#34763)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Defs.lean

added theorem Asymptotics.IsBigO.antisymm

added theorem Asymptotics.IsTheta.isBigO

added theorem Asymptotics.IsTheta.isBigO_symm

added def Asymptotics.IsTheta

Modified Mathlib/Analysis/Asymptotics/TVS.lean

added theorem Asymptotics.isThetaTVS_iff_isTheta

Modified Mathlib/Analysis/Asymptotics/Theta.lean

deleted theorem Asymptotics.IsBigO.antisymm

deleted theorem Asymptotics.IsTheta.isBigO

deleted theorem Asymptotics.IsTheta.isBigO_symm

deleted def Asymptotics.IsTheta