fderiv_continuousAlternatingMap_apply_const

English

Let hxs UniqueDiffWithinAt, hc DifferentiableWithinAt, u, m as above; then (fderivWithin 𝕜 (λ y, (c y) u) s x) m equals (fderivWithin 𝕜 c s x) m u.

Русский

Пусть hxs и hc как выше; тогда (fderivWithin ...) применение к m равно (fderivWithin c) применённому к m и u.

LaTeX

$$$\\forall hxs\\, hc\\, u\\, m:\\, (fderivWithin 𝕜 (λ y. (c(y))u) s x)\\, m = (fderivWithin 𝕜 c s x)\\, m\\, u.$$$

Lean4

theorem fderiv_continuousAlternatingMap_apply_const (hc : DifferentiableAt 𝕜 c x) (u : ι → F) :
    (fderiv 𝕜 (fun y ↦ (c y) u) x) = (fderiv 𝕜 c x).flipAlternating u :=
  (hc.hasFDerivAt.continuousAlternatingMap_apply_const u).fderiv

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