mul_const' — Mathlib

English

If a has strict derivative a' at x, then the map y ↦ a(y) b has derivative a' acting on b on the right.

Русский

Если функция a имеет строгую производную a' в точке x, то отображение y ↦ a(y) b имеет производную, равную правому умножению на b.

LaTeX

$$$\\forall ha\\, \\text{HasStrictFDerivAt } a\\ a'\\ x \\Rightarrow \\forall b:\\mathbb{𝔸}, \\text{HasStrictFDerivAt } (y \\mapsto a(y) b) (a' \\cdot b) x$$$

Lean4

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

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