sum — Mathlib

English

If every HasDerivWithinAt (A_i) (A'_i) s x holds for i in u, then HasDerivWithinAt of the sum function equals the sum of derivatives.

Русский

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

LaTeX

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

Lean4

theorem sum (h : ∀ i ∈ u, HasDerivWithinAt (A i) (A' i) s x) : HasDerivWithinAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) s x :=
  HasDerivAtFilter.sum h

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