isLittleO_zero_right_iff — Mathlib

English

There exists an inequality showing 0 is O_l(g) for any g, i.e., the zero function is of order not exceeding any bound.

Русский

Существуют неравенства, доказывающие, что 0 является Big-O по отношению к любому g.

LaTeX

$$$(f''=0)\\text{ is a Big-O of }g$$$

Lean4

@[simp]
theorem isLittleO_zero_right_iff : (f'' =o[l] fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0 :=
  ⟨fun h => isBigO_zero_right_iff.1 h.isBigO, fun h =>
    IsLittleO.of_isBigOWith fun _c _hc => isBigOWith_zero_right_iff.2 h⟩

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