sum_section — Mathlib

English

If finite many differentiable-at sections are given, their sum is differentiable at the point.

Русский

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

LaTeX

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

Lean4

theorem sum_section {ι : Type*} {s : Finset ι} {t : ι → (x : B) → E x} {x₀ : B}
    (hs : ∀ i, MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t i x)) x₀) :
    MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (∑ i ∈ s, (t i x))) x₀ :=
  by
  simp_rw [← mdifferentiableWithinAt_univ] at hs ⊢
  exact MDifferentiableWithinAt.sum_section hs

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