fun_sum — Mathlib

English

If for all i ∈ u, HasDerivAt (A_i) (A'_i) x, then HasDerivAt (y ↦ ∑ i∈u A_i(y)) (∑ i∈u A'_i) x.

Русский

Если для каждого i ∈ u выполняется HasDerivAt(A_i)(A'_i) x, то сумма имеет производную, равную сумме A'_i.

LaTeX

$$$\\forall i \\in u,\\ HasDerivAt(A_i, A'_i, x) \\Rightarrow HasDerivAt(\\lambda y. \\sum_{i\\in u} A_i(y), \\sum_{i\\in u} A'_i, x).$$$

Lean4

theorem fun_sum (h : ∀ i ∈ u, HasDerivAt (A i) (A' i) x) : HasDerivAt (fun y ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x :=
  HasDerivAtFilter.fun_sum h

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