fun_sum — Mathlib

English

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

Русский

Если для всех i∈u HasFDerivWithinAt(A_i)(A'_i) s x, то сумма имеет такую же производную внутри.

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 fun_sum (h : ∀ i ∈ u, HasFDerivAt (A i) (A' i) x) : HasFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x :=
  HasFDerivAtFilter.fun_sum h

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