Commit 2023-07-02 04:04 9d7fb19d

View on Github →

feat(Analysis/Asymptotics/AsymptoticEquivalent): add Trans instances for IsEquivalent (#5572) This PR adds several Trans instances for the IsEquivalent relation, and a few missing lemmas on the same topic.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

added theorem Asymptotics.IsBigO.trans_isEquivalent

added theorem Asymptotics.IsEquivalent.isTheta

added theorem Asymptotics.IsEquivalent.isTheta_symm

added theorem Asymptotics.IsEquivalent.trans_eventuallyEq

added theorem Asymptotics.IsEquivalent.trans_isBigO

added theorem Asymptotics.IsEquivalent.trans_isLittleO

added theorem Asymptotics.IsEquivalent.trans_isTheta

added theorem Asymptotics.IsLittleO.trans_isEquivalent

added theorem Asymptotics.IsTheta.trans_isEquivalent

modified theorem Filter.EventuallyEq.isEquivalent

added theorem Filter.EventuallyEq.trans_isEquivalent