smul_const — Mathlib

English

Let c: E → 𝕜' be differentiable at x with derivative c' at x. For any fixed f ∈ F, the function y ↦ c(y) · f is differentiable at x with derivative (Dc(x)) · f, i.e. (c' smulRight f).

Русский

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

LaTeX

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

Lean4

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

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