fun_sum — Mathlib

English

If for every i in a finite index set u, the function A_i has derivative A'_i at x, then the sum over i of A_i has derivative equal to the sum over i of A'_i at x.

Русский

Если для каждого i в конечном индексе u функция A_i имеет производную A'_i в точке x, то производная суммы ∑_{i∈u} A_i равна сумме производных ∑_{i∈u} A'_i в точке x.

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, HasDerivAtFilter (A i) (A' i) x L) :
    HasDerivAtFilter (fun y ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L := by
  simpa using (HasFDerivAtFilter.fun_sum h).hasDerivAtFilter

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