const_smul_section — Mathlib

English

If f is ContMDiffAt and s is ContMDiffAt, then x ↦ f(x) • s(x) is ContMDiffAt.

Русский

Если f и s гладки в точке x0, то x ↦ f(x) • s(x) гладко в точке x0.

LaTeX

$$ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (f x • (s x))) x0$$

Lean4

theorem const_smul_section (hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x₀) :
    ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (a • s x)) x₀ :=
  contMDiffAt_const.smul_section hs

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