continuousAlternatingMap_apply_const

English

If c is differentiable at x, then for every u the map y ↦ (c(y))u is differentiable at x with derivative given by (c'(·))(u).

Русский

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

LaTeX

$$$\\text{If } c: E \\to Alt^ι(F,G) \\text{ is differentiable at } x \\text{ with derivative } c', \\forall u, \\text{ differentiableAt } (\\lambda y. (c(y))(u)) \\; x \\text{ with derivative } (c'\\!)(u).$$$

Lean4

@[fun_prop]
theorem continuousAlternatingMap_apply_const (hc : DifferentiableAt 𝕜 c x) (u : ι → F) :
    DifferentiableAt 𝕜 (fun y ↦ (c y) u) x :=
  (hc.hasFDerivAt.continuousAlternatingMap_apply_const u).differentiableAt

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