# Commit 2020-01-08 13:16 92841c2e

View on Github →refactor(analysis/asymptotics): introduce `is_O_with`

(#1857)

- refactor(analysis/asymptotics): introduce
`is_O_with`

I use it to factor out common parts of the proofs of facts about`is_O`

and`is_o`

. It can also be used with`principal s`

filter to operate with`∀ x ∈ s, ∥f x∥ ≤ C * ∥g x∥`

is a manner similar to`is_O`

. - lint
- Fix compile
- Drop
`(s)mul_same`

lemmas. It's easy to use`(s)mul_is_O (is_O_refl _ _)`

or`(is_O_refl _ _).mul_is_o _`

instead - docs: say explicitly that
`is_O`

is better than`is_O_with`