continuousAlternatingMap_apply_const

English

If c is differentiableOn s at x, then y ↦ (c(y))u is differentiableOn s at x for every u.

Русский

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

LaTeX

$$$\\forall x\\in s,\\ \\text{DifferentiableWithinAt } c s x \\Rightarrow \\forall u, \\text{DifferentiableWithinAt } (\\lambda y. (c(y))u) s x.$$$

Lean4

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

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