isBigO_zero_right_iff — Mathlib

English

The zero function is Big-O of any g with respect to any l: 0 = O_l(g).

Русский

Нулевая функция является Big-O относительно любой функции g и любого фильтра l.

LaTeX

$$$(\\,0\\,)=O[l]\\ g$$$

Lean4

@[simp]
theorem isBigO_zero_right_iff : (f'' =O[l] fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0 :=
  ⟨fun h =>
    let ⟨_c, hc⟩ := h.isBigOWith
    isBigOWith_zero_right_iff.1 hc,
    fun h => (isBigOWith_zero_right_iff.2 h : IsBigOWith 1 _ _ _).isBigO⟩

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