sum — Mathlib

English

If UniqueDiffWithinAt 𝕜 s x and each A_i is differentiableWithinAt 𝕜 (A_i) s x, then fderivWithin 𝕜 (∑ i∈u A_i) s x equals ∑ i∈u fderivWithin 𝕜 (A_i) s x.

Русский

Если UniqueDiffWithinAt 𝕜 s x и каждый A_i дифференцируем внутри s в x, то производная внутри суммы равна сумме производных.

LaTeX

$$$\text{fderivWithin}_{\mathbb{k}}\left(\sum_{i\in u} A_i\right)\ s\ x = \sum_{i\in u} \text{fderivWithin}_{\mathbb{k}}\left(A_i\right)\ s\ x$$$

Lean4

@[simp, fun_prop]
theorem sum (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) : DifferentiableAt 𝕜 (∑ i ∈ u, A i) x :=
  HasFDerivAt.differentiableAt <| HasFDerivAt.sum fun i hi => (h i hi).hasFDerivAt

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