smul — Mathlib

English

Multiplying a C^n function by a constant on a set preserves C^n-ness: c • f is ContDiff 𝕜 n if f is ContDiff 𝕜 n.

Русский

Умножение на константу сохраняет гладкость: константа умножает C^n-функцию не изменяя её класса гладкости.

LaTeX

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

Lean4

/-- The scalar multiplication of two `C^n` functions at a point is `C^n` at this point. -/
@[fun_prop]
theorem smul {f : E → 𝕜} {g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    ContDiffAt 𝕜 n (fun x => f x • g x) x := by rw [← contDiffWithinAt_univ] at *; exact hf.smul hg

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