sum — Mathlib

English

If for all i ∈ u, HasFDerivAt (A_i) (A'_i) x, then HasFDerivAt (∑ i∈u A_i) (∑ i∈u A'_i) x.

Русский

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

LaTeX

$$$\operatorname{HasFDerivAt}\left(\sum_{i\in u} A_i\right)\left(\sum_{i\in u} A'_i\right)\ x$$

Lean4

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

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