sum_section — Mathlib

English

For a locally finite family of sections t_i, ContMDiffOn of their sum holds.

Русский

Для локально конечной совокупности секций выполняется гладкость суммы.

LaTeX

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

Lean4

theorem sum_section {s : Finset ι}
    (hs : ∀ i ∈ s, 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 ∈ s, (t i x))) u := fun x₀ hx₀ ↦
  .sum_section fun i hi ↦ hs i hi x₀ hx₀

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