fderivWithin_continuousMultilinear_apply_const

English

If c is differentiable within s at x and u is differentiable within s at x, then 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

theorem fderivWithin_continuousMultilinear_apply_const (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ∀ i, M i) :
    fderivWithin 𝕜 (fun y ↦ (c y) u) s x = ((fderivWithin 𝕜 c s x).flipMultilinear u) :=
  (hc.hasFDerivWithinAt.continuousMultilinear_apply_const u).fderivWithin hxs

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