add — Mathlib

English

If f1 = o_l g and f2 = o_l g, then their sum f1+f2 is also o_l g.

Русский

Если f1 = o_l g и f2 = o_l g, то сумма f1+f2 тоже равна o_l g.

LaTeX

$$$ (f_1 =o[l] g) \\land (f_2 =o[l] g) \\Rightarrow (f_1 + f_2) =o[l] g $$$

Lean4

theorem add (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) : (fun x => f₁ x + f₂ x) =o[l] g :=
  IsLittleO.of_isBigOWith fun c cpos =>
    ((h₁.forall_isBigOWith <| half_pos cpos).add (h₂.forall_isBigOWith <| half_pos cpos)).congr_const (add_halves c)

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