finsum_section_of_locallyFinite — Mathlib

English

Under the locally finite hypothesis and pointwise smoothness of components, the finsum of a family of sections is ContMDiffAt the base point x0.

Русский

При локально конечной условии и гладкости каждой составляющей финсом сумма секций образует C^k на базе в точке x0.

LaTeX

$$$\operatorname{LocallyFinite}\,\bigl(i \mapsto \{x \in M \mid t_i(x) \neq 0\}\bigr) \Rightarrow \; \text{ContMDiffAt } I (I.prod 𝓘(𝕜, F)) n (x \mapsto TotalSpace.mk' F x (\sum' i, t_i(x))) x_0$$$

Lean4

theorem finsum_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 ContMDiffWithinAt.finsum_section_of_locallyFinite ht ht'

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