smul_const_section — Mathlib

English

If a function f and a section s are differentiable on a set u, then the section x ↦ f(x) · s(x) is differentiable on u.

Русский

Если f и секция s дифференциируемы на u, то секция x ↦ f(x) · s(x) дифференцируема на u.

LaTeX

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

Lean4

theorem smul_const_section (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 (a • s x)) u :=
  .smul_section mdifferentiableOn_const hs

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