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, то их конечная сумма имеет производную.

LaTeX

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

Lean4

@[fun_prop]
theorem sum (h : ∀ i ∈ u, HasFDerivAt (A i) (A' i) x) : HasFDerivAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x :=
  HasFDerivAtFilter.sum h

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