smul_const — Mathlib

English

Let c: E → 𝕜' have derivative c' within s at x. Then the map y ↦ c(y) · f has derivative within s at x given by c'.smulRight f.

Русский

Пусть c: E → 𝕜' имеет производную внутри множества s в точке x, тогда функция y ↦ c(y) · f имеет производную внутри s в x, равную c'.smulRight f.

LaTeX

$$$\HasFDerivWithinAt\ c\ c'\ s\ x \Rightarrow \HasFDerivWithinAt\ (\\lambda y. c(y) \\cdot f)\ (c'.smulRight f)\ s\ x$$$

Lean4

@[fun_prop]
theorem smul_const (hc : HasFDerivWithinAt c c' s x) (f : F) :
    HasFDerivWithinAt (fun y => c y • f) (c'.smulRight f) s x := by
  simpa only [smul_zero, zero_add] using hc.smul (hasFDerivWithinAt_const f x s)

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