fun_sum — Mathlib

English

Under UniqueDiffWithinAt and differentiability of each A_i within s, the derivative within s of the sum equals the sum of derivatives within s.

Русский

При UniqueDiffWithinAt и дифференцируемости каждого A_i внутри s производная внутри суммы равна сумме производных.

LaTeX

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

Lean4

@[fun_prop]
theorem fun_sum (h : ∀ i ∈ u, DifferentiableOn 𝕜 (A i) s) : DifferentiableOn 𝕜 (fun y => ∑ i ∈ u, A i y) s :=
  fun x hx => DifferentiableWithinAt.fun_sum fun i hi => h i hi x hx

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