fun_sum — Mathlib

English

If for each i ∈ u, DifferentiableWithinAt 𝕜 (A_i) s x, then DifferentiableWithinAt 𝕜 (∑ i∈u A_i) s x.

Русский

Если для каждого i∈u функция A_i дифференцируема внутри s в x, тогда их сумма дифференцируема внутри s в x.

LaTeX

$$$\operatorname{DifferentiableWithinAt}_{\mathbb{k}}\left(\sum_{i\in u} A_i\right)\ s\ x$$

Lean4

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

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