sum_section_of_locallyFinite — Mathlib

English

If a family of differentiable sections indexed by Finset is given, their Finset-sum is differentiable.

Русский

Если дана семья дифференцируемых секций, индексируемая Finset сумма дифференцируема.

LaTeX

$$$ MDifferentiable I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (s.sum (λ i, t i x)))$$

Lean4

/-- The sum of a locally finite collection of sections is differentiable if each section is. -/
theorem sum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : B | t i x ≠ 0})
    (ht' : ∀ i, MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t i x))) :
    MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (∑' i, (t i x))) := fun x ↦
  .sum_section_of_locallyFinite ht fun i ↦ ht' i x

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