Commit 2020-10-30 02:02 581b2af3
View on Github →feat(analysis/asymptotics): Equivalent definitions for is_[oO] u v l looking like u = φ * v for some φ (#4646)
The advantage of these statements over u/v tendsto 0 / is bounded is they do not require any nonvanishing assumptions about v