add_isBigOWith — Mathlib

English

If h1 = OWith c1 l f1 g and h2 = o_l f2 g with c1 < c2, then h1 - h2 is in OWith c2 l (f1 - f2) g.

Русский

Если h1 = OWith c1 l f1 g и h2 = o_l f2 g при c1 < c2, то h1 - h2 ∈ OWith c2 l (f1 - f2) g.

LaTeX

$$$ (h_1 :\\ IsBigOWith c_1 l f_1 g) \\land (h_2 : f_2 =o[l] g) \\land (c_1 < c_2) \\Rightarrow IsBigOWith c_2 l (f_1 - f_2) g $$$

Lean4

theorem add_isBigOWith (h₁ : f₁ =o[l] g) (h₂ : IsBigOWith c₁ l f₂ g) (hc : c₁ < c₂) :
    IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g :=
  (h₂.add_isLittleO h₁ hc).congr_left fun _ => add_comm _ _

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