sum_section — Mathlib

English

If ht is LocallyFinite and ht' gives ContMDiffAt for each t_i at x0, then sum is ContMDiffAt at x0.

Русский

Если ht — локально конечно, и ht' даёт гладкость каждой t_i в x0, то сумма гладкая в x0.

LaTeX

$$ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (tsum fun i => t i x)) x0$$

Lean4

theorem sum_section {s : Finset ι} {x₀ : M}
    (hs : ∀ i ∈ s, ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t i x)) x₀) :
    ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (∑ i ∈ s, (t i x))) x₀ :=
  by
  simp_rw [← contMDiffWithinAt_univ] at hs ⊢
  exact .sum_section hs

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