mdifferentiableWithinAt_smul_const_section

English

If a section s is differentiable and f is a differentiable scalar function, then the product f · s is differentiable as a section.

Русский

Если секция s дифференцируема и функция f дифференцируема как скаляр, то произведение f · s дифференцируемо как секция.

LaTeX

$$$ MDifferentiable I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (f x \cdot s x))$$

Lean4

theorem mdifferentiableWithinAt_smul_const_section
    (hs : MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u x₀) :
    MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (a • s x)) u x₀ :=
  .smul_section mdifferentiableWithinAt_const hs

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