const_mul — Mathlib

English

If a has a strict Fréchet derivative a′ at x, then the map y ↦ c(y) d has a strict Fréchet derivative equal to d multiplied by a′, i.e. HasStrictFDerivAt (fun y => c(y) d) (d • a′) x.

Русский

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

LaTeX

$$$\\text{HasStrictFDerivAt }\\big( a, a', x \\big) \\Rightarrow \\text{HasStrictFDerivAt }\\big( \\lambda y. c(y) \\cdot d, \\ d \\cdot a', x \\big)$$$

Lean4

@[fun_prop]
theorem const_mul (ha : HasStrictFDerivAt a a' x) (b : 𝔸) : HasStrictFDerivAt (fun y => b * a y) (b • a') x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸) b).hasStrictFDerivAt.comp x ha

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