smul — Mathlib

English

The operation of multiplying a C^n function by a constant is C^n in the target; same as contDiff_const_smul applied globally.

Русский

Операция умножения C^n-функции на константу сохраняет гладкость.

LaTeX

$$$\\\\forall c \\\\in R, \\\\ContDiff 𝕜 n f \\\\Rightarrow \\\\ContDiff 𝕜 n (\\\\lambda x. c \\\\cdot f(x))$$

Lean4

/-- The scalar multiplication of two `C^n` functions is `C^n`. -/
@[fun_prop]
theorem smul {f : E → 𝕜} {g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun x => f x • g x :=
  contDiff_smul.comp (hf.prodMk hg)

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