sum — Mathlib

English

Under UniqueDiffWithinAt, the derivative within s of a sum equals the sum of derivatives within s.

Русский

При UniqueDiffWithinAt производная внутри s суммы равна сумме производных внутри 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

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

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