continuousMultilinear_apply_const

English

If c is differentiable within s at x and u is differentiable within s at x, then the product y ↦ (c(y))(u(y)) is differentiable within s at x.

Русский

Если c дифференцируема внутри s в x и u дифференцируема внутри s в x, то f(y)=c(y)(u(y)) дифференцируема внутри s в x.

LaTeX

$$$ \operatorname{DifferentiableWithinAt}_{\mathbb{K}} c s x \land \operatorname{DifferentiableWithinAt}_{\mathbb{K}} u s x \Rightarrow \operatorname{DifferentiableWithinAt}_{\mathbb{K}}\bigl( y \mapsto (c(y))(u(y)) \bigr) s x$$$

Lean4

@[fun_prop]
theorem continuousMultilinear_apply_const (hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) :
    DifferentiableAt 𝕜 (fun y ↦ (c y) u) x :=
  (hc.hasFDerivAt.continuousMultilinear_apply_const u).differentiableAt

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