const_smul — Mathlib

English

The iterated derivative within a set commutes with scalar multiplication at a point x: (a • f)^(i) = a • f^(i) at x.

Русский

Итеративная производная внутри множества коммутирует с умножением на константу: D^i(a f) = a D^i f.

LaTeX

$$$\\\\iteratedFDerivWithin 𝕜 i (a \\\\cdot f) s x = a \\\\cdot \\\\ iteratedFDerivWithin 𝕜 i f s x$$

Lean4

/-- The scalar multiplication of a constant and a `C^n` function at a point is `C^n` at this
point. -/
@[fun_prop]
theorem const_smul {f : E → F} {x : E} (c : R) (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun y => c • f y) x := by
  rw [← contDiffWithinAt_univ] at *; exact hf.const_smul c

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