smul_section — Mathlib

English

If a family of differentiable sections indexed by a set I is differentiable on a set u, then the sum of these sections is differentiable on u.

Русский

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

LaTeX

$$$ MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (\sum_{i} t_i x)) u$$

Lean4

theorem smul_section (hf : MDifferentiableOn I 𝓘(𝕜) f u)
    (hs : MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u) :
    MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (f x • s x)) u := fun x₀ hx₀ ↦
  .smul_section (hf x₀ hx₀) (hs x₀ hx₀)

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