triangle — Mathlib

English

Let f1, f2, f3: α → E′ and g: α → F′ be functions with respect to l. If f1 − f2 = o_l(g) and f2 − f3 = o_l(g), then f1 − f3 = o_l(g).

Русский

Пусть f1, f2, f3: α → E′ и g: α → F′. Если f1 − f2 = o_l(g) и f2 − f3 = o_l(g), тогда f1 − f3 = o_l(g).

LaTeX

$$$\\,(f_1-f_3)=o[l](g)\\,$$$

Lean4

theorem triangle (h₁ : (fun x => f₁ x - f₂ x) =o[l] g) (h₂ : (fun x => f₂ x - f₃ x) =o[l] g) :
    (fun x => f₁ x - f₃ x) =o[l] g :=
  (h₁.add h₂).congr_left fun _x => sub_add_sub_cancel _ _ _

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