sum_section — Mathlib

English

The sum of a finite family of differentiable sections remains differentiable when viewed in a common trivialization.

Русский

Сумма конечного числа дифференцируемых секций сохраняет дифференцируемость при представлении в общей тривиализации.

LaTeX

$$$ MDifferentiable (I.prod (modelWithCornersSelf 𝕜 F)) (\x => TotalSpace.mk' F x (\sum i ∈ S, t_i x))$$

Lean4

theorem sum_section {ι : Type*} {s : Finset ι} {t : ι → (x : B) → E x}
    (hs : ∀ 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 ∈ s, (t i x))) := fun x₀ ↦
  .sum_section fun i ↦ (hs i) x₀

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