contMDiff_sum — Mathlib

English

If (f_i) is a locally finite family of smooth functions f_i: M → ℝ, then the summed function x ↦ ∑ᶠ_i f_i(x) is ContMDiff of all orders.

Русский

Если семейство из локально конечного числа функций f_i: M → ℝ, каждая из которых бесконечно дифференцируема, то сумма ∑ᶠ_i f_i(x) бесконечно дифференцируема.

LaTeX

$$$\text{If } (f_i)_{i\in ι} \text{ is locally finite with each } f_i: M \to ℝ \\text{contMDiff of all orders holds for } x \mapsto \sum^\infty_i f_i(x).$$$

Lean4

theorem contMDiff_sum : ContMDiff I 𝓘(ℝ) ∞ fun x => ∑ᶠ i, f i x :=
  contMDiff_finsum (fun i => (f i).contMDiff) f.locallyFinite

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