add_isLittleO — Mathlib

English

If f1 = OWith c1 l f g and f2 = OWith c2 l f' g, then their sum is OWith (c1+c2) l (f+f') relative to g.

Русский

Если f1 = OWith c1 l f g и f2 = OWith c2 l f' g, то их сумма равна OWith (c1+c2) l (f+f').

LaTeX

$$$ (f_1 =OWith c_1 l f g) \\land (f_2 =OWith c_2 l f' g) \\Rightarrow (f_1 + f_2) =OWith (c_1+c_2) l (f+f') $$$

Lean4

theorem add_isLittleO (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
    IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g :=
  (h₁.add (h₂.forall_isBigOWith (sub_pos.2 hc))).congr_const (add_sub_cancel _ _)

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