deriv_fun_sum — Mathlib

English

If for all i ∈ u, DifferentiableAt 𝕜 (A_i) x holds, then deriv (sum_i A_i) x equals sum_i deriv (A_i) x.

Русский

Если для каждого i ∈ u функция A_i дифференцируема в x, то производная суммы равна сумме производных.

LaTeX

$$$\\forall i \\in u,\\ DifferentiableAt 𝕜 (A_i) x \\Rightarrow deriv(\\sum_{i\\in u} A_i)(x) = \\sum_{i\\in u} deriv(A_i)(x).$$$

Lean4

@[simp]
theorem deriv_fun_sum (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) :
    deriv (fun y ↦ ∑ i ∈ u, A i y) x = ∑ i ∈ u, deriv (A i) x :=
  (HasDerivAt.fun_sum fun i hi ↦ (h i hi).hasDerivAt).deriv

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