const_mul — Mathlib

English

If a has a Fréchet derivative a′ within a set s at x, then the map y ↦ c(y) d has a Frechet derivative within s at x given by d • a′.

Русский

Если у a есть производная Фрéше внутри множества s в точке x, то отображение y ↦ c(y) d имеет производную внутри s в x, равную d • a′.

LaTeX

$$$\\operatorname{fderivWithin}_{\\mathbb{K}}\\big( \\lambda y. c(y) \\cdot d, s, x \\big) \\\\ =\\ d \\cdot \\operatorname{fderivWithin}_{\\mathbb{K}}(c, s, x)$$$

Lean4

@[fun_prop]
theorem const_mul (ha : HasFDerivWithinAt a a' s x) (b : 𝔸) : HasFDerivWithinAt (fun y => b * a y) (b • a') s x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸) b).hasFDerivAt.comp_hasFDerivWithinAt x ha

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