sum_section_of_locallyFinite — Mathlib

English

If a finite family of ContMDiffOn sections t_i is given, then their sum is ContMDiffOn.

Русский

Если дано конечное семейство секций t_i, каждая из которых ContMDiffOn, то их сумма ContMDiffOn.

LaTeX

$$ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s.sum fun i => t i x)) u$$

Lean4

/-- The sum of a locally finite collection of sections is `C^k` on a set `u` iff each section is. -/
theorem sum_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 ↦
  .sum_section_of_locallyFinite ht (ht' · x hx)

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