continuousAlternatingMap_apply_const

English

If c is differentiable within at x on s with derivative c', then y ↦ (c(y))u is differentiable within at x for every fixed u.

Русский

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

LaTeX

$$$\\text{If } c: E \\to Alt^ι(F,G) \\text{ is differentiableWithinAt } c' \\text{ at } x \\text{ on } s, \\forall u, \\text{ differentiableWithinAt } (\\lambda y. (c(y))(u)) \\; s \\ x.$$$

Lean4

@[fun_prop]
theorem continuousAlternatingMap_apply_const (hc : DifferentiableWithinAt 𝕜 c s x) (u : ι → F) :
    DifferentiableWithinAt 𝕜 (fun y ↦ (c y) u) s x :=
  (hc.hasFDerivWithinAt.continuousAlternatingMap_apply_const u).differentiableWithinAt

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