Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-06 20:46 d0b7ecc9

View on Github →

refactor(analysis/asymptotics): rename is_O.join to is_O.sup (#14558)

rename is_*.join to is_*.sup;
add iff versions.

Estimated changes

Modified src/analysis/asymptotics/asymptotics.lean

deleted theorem asymptotics.is_O.join

added theorem asymptotics.is_O.sup

added theorem asymptotics.is_O_sup

deleted theorem asymptotics.is_O_with.join'

deleted theorem asymptotics.is_O_with.join

added theorem asymptotics.is_O_with.sup'

added theorem asymptotics.is_O_with.sup

deleted theorem asymptotics.is_o.join

added theorem asymptotics.is_o.sup

added theorem asymptotics.is_o_sup

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/fderiv.lean

Modified src/analysis/complex/phragmen_lindelof.lean