sum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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