right_isBigO_add' — Mathlib

English

If a function f: α → ∀ i, E_i has a bound C on a tail, then for each i the bound holds uniformly with the same C.

Русский

Если функция f: α → ∀ i, E_i имеет предел сверху C на хвосте, то для каждого i граница одинакова по всем компонентам.

LaTeX

$$$\\displaystyle f = O_l \\ g' \\iff \\forall i, f(\\cdot)(i) = O_l g'(\\cdot).$$$

Lean4

theorem right_isBigO_add' {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] (f₂ + f₁) :=
  add_comm f₁ f₂ ▸ h.right_isBigO_add

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