triangle — Mathlib

English

Let f1, f2, f3 be functions from α to appropriate normed spaces, and g a reference function, with along a filter l we have f1 − f2 = O_l(g) with constant c and f2 − f3 = O_l(g) with constant c'. Then f1 − f3 = O_l(g) with constant c + c'.

Русский

Пусть f1, f2, f3: α → E′ и g: α → F′; при любом фильтре l если f1 − f2 = O_l(g) с константой c и f2 − f3 = O_l(g) с константой c', тогда f1 − f3 = O_l(g) с константой c + c'.

LaTeX

$$$\\mathrm{IsBigOWith}(c+c',\\ l\\,)(f_1-f_3)\\,g$$$

Lean4

theorem triangle (h₁ : IsBigOWith c l (fun x => f₁ x - f₂ x) g) (h₂ : IsBigOWith c' l (fun x => f₂ x - f₃ x) g) :
    IsBigOWith (c + c') l (fun x => f₁ x - f₃ x) g :=
  (h₁.add h₂).congr_left fun _x => sub_add_sub_cancel _ _ _

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