sub — Mathlib

English

If f2 = O[l] g, then f1+(-f2) has the same Big-O behavior as f1; equivalently, (f1 - f2) = O[l] g iff f1 = O[l] g.

Русский

Если f2 = O[l] g, то f1 + (-f2) имеет такую же Big-O-однородность как f1; эквивалентно, (f1 - f2) = O[l] g, если f1 = O[l] g.

LaTeX

$$$ (f_2 =O[l] g) \\Rightarrow (f_1 + f_2) =O[l] g \\Leftrightarrow (f_1 =O[l] g) $$$

Lean4

theorem sub (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) : (fun x => f₁ x - f₂ x) =O[l] g := by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

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