English
Let c: E → Alt^ι(F, G) be differentiable within a set s at x with derivative c'. Then, for every fixed ι-indexed family u: ι → F, the map y ↦ (c(y))(u) is differentiable within s at x, and its derivative is given by the linear map h ↦ (c'(h))(u) (equivalently, (c'.flipAlternating u))(h).
Русский
Пусть c: E → Alt^ι(F, G) дифференцируем внутри s в точке x с производной c'. Тогда для любого фиксированного семейства u: ι → F функция y ↦ (c(y))(u) дифференцируема внутри s в x, и её производная равна отображению h ↦ (c'(h))(u) (то же самое, как (c'.flipAlternating u))(h).
LaTeX
$$$\\forall u:\\, \\iota \\to F,\\; HasFDerivWithinAt\\; c\\; c'\\; s\\; x\\Rightarrow HasFDerivWithinAt\\; (\\lambda y. (c(y))(u))\\; (\\text{flip}(c',u))\\; s\\ x$$$
Lean4
@[fun_prop]
theorem continuousAlternatingMap_apply_const (hc : HasFDerivWithinAt c c' s x) (u : ι → F) :
HasFDerivWithinAt (c · u) (c'.flipAlternating u) s x :=
(ContinuousAlternatingMap.apply 𝕜 F G u).hasFDerivAt.comp_hasFDerivWithinAt x hc
