isBigO_zero — Mathlib

English

For any f′: α → E′ and g′: α → F′, the difference f′ − f′ is trivially zero, hence is Big-O of g′ along l.

Русский

Для любых f′: α → E′ и g′: α → F′ разность f′ − f′ тождественно равна нулю, следовательно, является Big-O по g′ вдоль l.

LaTeX

$$$(f'-f')=O[l]\\,g'$$$$

Lean4

theorem isBigO_zero : (fun _x => (0 : E')) =O[l] g :=
  isBigO_iff_isBigOWith.2 ⟨0, isBigOWith_zero' _ _⟩

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