contDiff_const_smul — Mathlib

English

The scalar multiple by a constant is smooth in the domain: c • f is ContDiff 𝕜 n on s if f is ContDiff 𝕜 n on s.

Русский

Умножение на константу сохраняет гладкость на данной области.

LaTeX

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

Lean4

@[fun_prop]
theorem contDiff_const_smul (c : R) : ContDiff 𝕜 n fun p : F => c • p :=
  (c • ContinuousLinearMap.id 𝕜 F).contDiff

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