mul_const — Mathlib

English

If ha is differentiable at x, then the map y ↦ a(y) * b is differentiable at x.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem mul_const (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) : DifferentiableAt 𝕜 (fun y => a y * b) x :=
  (ha.hasFDerivAt.mul_const' b).differentiableAt

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