fderivWithin_continuousAlternatingMap_apply_const

English

For hxs unique differentiability at x, we have fderivWithin of y ↦ (c(y))u evaluated at m equals fderivWithin of c at x applied to m and then to u.

Русский

Для уникального дифференцирования в x внутри s выполняется равенство: дифференциал внутри fderivWithin y ↦ (c(y))u в направлении m равен применению производной c к m и затем к u.

LaTeX

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

Lean4

theorem fderivWithin_continuousAlternatingMap_apply_const (hxs : UniqueDiffWithinAt 𝕜 s x)
    (hc : DifferentiableWithinAt 𝕜 c s x) (u : ι → F) :
    fderivWithin 𝕜 (fun y ↦ (c y) u) s x = ((fderivWithin 𝕜 c s x).flipAlternating u) :=
  (hc.hasFDerivWithinAt.continuousAlternatingMap_apply_const u).fderivWithin hxs

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