sum_section_of_locallyFinite — Mathlib

English

If ht is LocallyFinite and ht' provides ContMDiffAt for each t_i on x, then the sum ∑' t_i is ContMDiffAt at x.

Русский

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

LaTeX

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

Lean4

/-- The sum of a locally finite collection of sections is `C^k` at `x` iff each section is. -/
theorem sum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : M | t i x ≠ 0})
    (ht' : ∀ i, 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, (t i x))) x₀ :=
  by
  simp_rw [← contMDiffWithinAt_univ] at ht' ⊢
  exact .sum_section_of_locallyFinite ht ht'

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