continuousAlternatingMap_apply_const

English

If c is differentiable, then for every u the map y ↦ (c(y))u is differentiable with derivative as above.

Русский

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

LaTeX

$$$\\text{Differentiable } c \\Rightarrow \\forall u,\\text{Differentiable } (\\lambda y. (c(y))u).$$$

Lean4

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

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