mul_const — Mathlib

English

If ha is differentiable within s at x, then the map y ↦ a(y) * b is differentiable within s at x with derivative a' • b.

Русский

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

LaTeX

$$$\\text{DifferentiableWithinAt}_{\\mathbb{K}}(a,s) \\Rightarrow \\text{DifferentiableWithinAt}_{\\mathbb{K}}(y \\mapsto a(y) b,s, x)$$$

Lean4

@[fun_prop]
theorem mul_const (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) : DifferentiableWithinAt 𝕜 (fun y => a y * b) s x :=
  (ha.hasFDerivWithinAt.mul_const' b).differentiableWithinAt

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