add — Mathlib

English

If a family of functions f_i is little-o of g for every i, then the function x ↦ f_i(x) across all i is little-o of g.

Русский

Если для каждой i функция f_i = o(g), то функция x ↦ f_i(x) по индексу i равна o(g).

LaTeX

$$$\forall i,\ f_i =o_{𝕜;l} g \Rightarrow (x,i) \mapsto f_i(x) =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_isLittleOTVS <| h₁.prodMk h₂

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