add — Mathlib

English

If f1 =o(g) and f2 =o(g) along l, then their sum f1 + f2 is o(g).

Русский

Если f1 = o(g) и f2 = o(g) вдоль l, то сумма f1 + f2 = o(g).

LaTeX

$$$ f_1 =o_{𝕜;l} g \quad \text{and} \quad f_2 =o_{𝕜;l} g \quad \Rightarrow \quad f_1+f_2 =o_{𝕜;l} g.$$$

Lean4

theorem add [ContinuousAdd E] [ContinuousSMul 𝕜 E] {f₁ f₂ : α → E} {g : α → F} {l : Filter α} (h₁ : f₁ =O[𝕜; l] g)
    (h₂ : f₂ =O[𝕜; l] g) : (f₁ + f₂) =O[𝕜; l] g :=
  ContinuousLinearMap.fst 𝕜 E E + ContinuousLinearMap.snd 𝕜 E E |>.isBigOTVS_comp |>.trans <| h₁.prodMk h₂

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