sum — Mathlib

English

If each HasStrictDerivAt (A_i) (A'_i) holds for i ∈ u, then HasStrictDerivAt of the sum equals the sum of derivatives.

Русский

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

LaTeX

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

Lean4

theorem sum (h : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x) : HasStrictDerivAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x := by
  simpa using (HasStrictFDerivAt.sum h).hasStrictDerivAt

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