sum — Mathlib

English

The sum of finitely many C^n functions is C^n.

Русский

Сумма конечного числа функций C^n также является C^n.

LaTeX

$$ContDiff 𝕜 n f_1 \ldots f_m \Rightarrow ContDiff 𝕜 n (\sum_{i=1}^m f_i)$$

Lean4

@[fun_prop]
theorem sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E} {x : E}
    (h : ∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun x => f i x) t x) : ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) t x := by
  classical
    induction s using Finset.induction_on with
  | empty => simp [contDiffWithinAt_const]
  | insert i s is IH =>
    simp only [is, Finset.sum_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i s)).add (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))

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