sum_section — Mathlib

English

If a family of differentiable sections indexed by a finite set s is differentiable on a set u, then their sum is differentiable on u.

Русский

Если семейство секций, индексируемых по конечному множеству, дифференцируемо на u, то их сумма дифференцируема на u.

LaTeX

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

Lean4

theorem sum_section {ι : Type*} {s : Finset ι} {t : ι → (x : B) → E x}
    (hs : ∀ i, MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t i x)) u) :
    MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (∑ i ∈ s, (t i x))) u := fun x₀ hx₀ ↦
  .sum_section fun i ↦ hs i x₀ hx₀

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