Commit 2026-01-27 15:05 cb7ef5d6

View on Github →

feat(Asymptotics/TVS): define IsThetaTVS (#34033)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/TVS.lean

modified theorem Asymptotics.IsBigOTVS.trans

modified theorem Asymptotics.IsBigOTVS.trans_isLittleOTVS

added theorem Asymptotics.IsBigOTVS.trans_isThetaTVS

modified theorem Asymptotics.IsLittleOTVS.trans

modified theorem Asymptotics.IsLittleOTVS.trans_isBigOTVS

added theorem Asymptotics.IsLittleOTVS.trans_isThetaTVS

added theorem Asymptotics.IsThetaTVS.isBigOTVS

added theorem Asymptotics.IsThetaTVS.symm

added theorem Asymptotics.IsThetaTVS.trans

added theorem Asymptotics.IsThetaTVS.trans_isBigOTVS

added theorem Asymptotics.IsThetaTVS.trans_isLittleOTVS

added def Asymptotics.IsThetaTVS

added theorem Asymptotics.isThetaTVS_comm

added theorem ContinuousLinearMap.isThetaTVS_comp