mono — Mathlib

English

If h is Big-O along l with a looser filter l', then f = O[l] g from h and monotone l ≤ l'.

Русский

Если существует ограничение Big-O по более слабому фильтру l', то зная, что l ≤ l', получаем f = O[l] g.

LaTeX

$$$ IsBigOWith\ c\ l' f g \to\ (l \le l') \Rightarrow IsBigOWith\ c\ l f g $$$

Lean4

theorem mono (h : f =O[l'] g) (hl : l ≤ l') : f =O[l] g :=
  isBigO_iff_isBigOWith.2 <| h.isBigOWith.imp fun _c h => h.mono hl

Похожие утверждения