const_smul — Mathlib

English

Iterated derivatives commute with scalar multiplication by a fixed scalar a: applying a to the iterated derivative of a function is the same as multiplying the iterated derivative by a.

Русский

Поверка итеративных производных и умножение на константу коммутируют: a ∙ D^i f = D^i (a ∙ 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 within a set at a point is `C^n`
within this set at this point. -/
@[fun_prop]
theorem const_smul {s : Set E} {f : E → F} {x : E} (c : R) (hf : ContDiffWithinAt 𝕜 n f s x) :
    ContDiffWithinAt 𝕜 n (fun y => c • f y) s x :=
  (contDiff_const_smul c).contDiffAt.comp_contDiffWithinAt x hf

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