English
For the space PiLp p E consisting of families f = (f_i) indexed by ι into the corresponding spaces E_i, the map sending f to its i-th coordinate f_i is Frechet differentiable at every f, and its derivative is the i-th projection onto E_i.
Русский
Для пространства PiLp p E, состоящего из семейств f = (f_i), где i пробегает по ι, отображение f ↦ f_i является где-то дифференцируемым по Фреше в любой точке f, причем его производная равна i-й проекции на E_i.
LaTeX
$$$ \text{HasStrictFDerivAt}\big( f \mapsto f_i \big)\big( \pi_i \big)\, f $$$
Lean4
nonrec theorem hasStrictFDerivAt_apply (f : PiLp p E) (i : ι) :
HasStrictFDerivAt (𝕜 := 𝕜) (fun f : PiLp p E => f i) (proj p E i) f :=
(hasStrictFDerivAt_apply i f).comp f (hasStrictFDerivAt_ofLp (𝕜 := 𝕜) p f)
