sum — Mathlib

English

If each A_i has derivative A'_i at x with respect to the filter L, then the sum over i ∈ u of A_i has derivative equal to the sum of A'_i at x with respect to L.

Русский

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

LaTeX

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

Lean4

theorem sum (h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) x L) : HasDerivAtFilter (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x L :=
  by
  convert HasDerivAtFilter.fun_sum h
  simp

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