sum — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{HasFDerivAtFilter}_{\mathbb{k}}\left(\sum_{i\in u} A_i\right)\left(\sum_{i\in u} A'_i\right)\ x\ L$$

Lean4

@[fun_prop]
theorem sum (h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) : HasStrictFDerivAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x := by
  convert HasStrictFDerivAt.fun_sum h; simp

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