finsum_section_of_locallyFinite — Mathlib

English

If a locally finite family of sections has C^k regularity on M, then their finsum is a C^k section on the whole set u.

Русский

Если совокупность секций локально конечна и каждая секция имеет гладкость C^k на M, то их финсом образует C^k секцию на заданном множестве u.

LaTeX

$$$\operatorname{LocallyFinite} (i \mapsto \{x \in M \mid t_i(x) \neq 0\}) \Rightarrow \; \ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (x \mapsto \mathrm{TotalSpace.mk'} F x (\sum' i, t_i(x))) u$$$

Lean4

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

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