Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-04 12:05 0aed8b1e

View on Github →

refactor(analysis/asymptotics): make definitions immediately irreducible (#6021)

Estimated changes

Modified src/analysis/asymptotics.lean

modified theorem asymptotics.is_O.add

added theorem asymptotics.is_O.bound

added theorem asymptotics.is_O.is_O_with

modified theorem asymptotics.is_O_top

modified theorem asymptotics.is_O_with.is_O

deleted theorem asymptotics.is_O_with.of_bound

modified theorem asymptotics.is_O_with_bot

modified theorem asymptotics.is_O_with_top

modified theorem asymptotics.is_O_zero

modified theorem asymptotics.is_o.is_O_with

modified theorem asymptotics.is_o_bot