English
Let f: H → ℝ^ι be a function into a finite-dimensional Euclidean space and f' its Fréchet derivative at y with respect to a set t. Then f has derivative f' within t at y if and only if, for every coordinate i, the i-th coordinate function x ↦ f(x)_i has derivative given by the composition of f' with the i-th projection; i.e. HasFDerivWithinAt (fun x => f(x)_i) (Proj_i ∘ f') within t at y for all i.
Русский
Пусть f: H → ℝ^ι. Тогда производная Фреше внутри множества t в точке y существет тогда и только тогда, когда каждая координатная функция f_i имеет производную внутри t, и её производная равна композиции проекции на i-ую координату с f'.
LaTeX
$$$\\text{HasFDerivWithinAt } f\\, f'\\, t\\, y \\Longleftrightarrow \\forall i, \\text{HasFDerivWithinAt} (\\lambda x, f(x)_i) \\big( \\mathrm{Proj}_i \\circ f'\\big)\\, t\\, y$$$
Lean4
theorem hasFDerivWithinAt_euclidean :
HasFDerivWithinAt f f' t y ↔ ∀ i, HasFDerivWithinAt (fun x => f x i) (PiLp.proj _ _ i ∘L f') t y :=
hasFDerivWithinAt_piLp _
