continuousAlternatingMap_apply_const

English

If c is differentiable within at x with derivative c', then for any fixed u, the function y ↦ (c(y))u has derivative at x equal to (c'.flipAlternating u).

Русский

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

LaTeX

$$$\\text{If } c: E \\to Alt^ι(F,G) \\text{ is differentiable within } s \\text{ at } x \\text{ with derivative } c', \\text{ then } \\forall u,\\ HasFDerivWithinAt(\\lambda y. (c(y))(u), c'.flipAlternating(u))\\ s\\ x.$$$

Lean4

@[fun_prop]
theorem continuousAlternatingMap_apply_const (hc : HasFDerivAt c c' x) (u : ι → F) :
    HasFDerivAt (fun y ↦ (c y) u) (c'.flipAlternating u) x :=
  (ContinuousAlternatingMap.apply 𝕜 F G u).hasFDerivAt.comp x hc

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