const_smul — Mathlib

English

The scalar multiplication by a constant on a domain preserves ContDiff: c • f is ContDiff 𝕜 n if f is ContDiff 𝕜 n on that domain.

Русский

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

LaTeX

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

Lean4

/-- The scalar multiplication of a constant and a `C^n` function is `C^n`. -/
@[fun_prop]
theorem const_smul {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun y => c • f y :=
  (contDiff_const_smul c).comp hf

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