finsum_section_of_locallyFinite — Mathlib

English

Let a locally finite family of sections t_i be smooth; the pointwise sum x ↦ ∑' i t_i(x) is a smooth section.

Русский

Пусть множество секций {t_i} локально конечна и гладкая; сумма по точкам x ↦ ∑' i t_i(x) образует гладкую секцию.

LaTeX

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

Lean4

theorem finsum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : M | t i x ≠ 0})
    (ht' : ∀ i, ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t i x))) :
    ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (∑ᶠ i, t i x)) := fun x ↦
  ContMDiffAt.finsum_section_of_locallyFinite ht fun i ↦ ht' i x

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