Commit 2023-09-08 11:01 db154ca0

View on Github →

feat: characterize isLittleO on principal filters (#7008) And use this to golf isLittleO_top.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.isLittleO_principal

modified theorem Asymptotics.isLittleO_top