mdifferentiable_smul_section — Mathlib

English

If a differentiable section s is given, then multiplying it by a constant scalar a yields a differentiable section a · s.

Русский

Если секция s дифференцируема, то секция a · s дифференцируема для любого константного скаляра a.

LaTeX

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

Lean4

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

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