English
Differentiability of a map Φ: E → ∀ i, F'i is equivalent to differentiability of all coordinates; equivalently, the product map is differentiable iff each coordinate map is differentiable.
Русский
Дифференцируемость Φ: E → ∀ i, F'i эквивалентна дифференцируемости всех координат; следовательно, произведение дифференцируемо тогда и только тогда, когда каждая координата дифференцируема.
LaTeX
$$$\\text{Differentiable } Φ \\iff \\forall i, \\text{Differentiable } Φ_i.$$$
Lean4
@[fun_prop]
theorem hasFDerivWithinAt_apply (i : ι) (f : ∀ i, F' i) (s' : Set (∀ i, F' i)) :
HasFDerivWithinAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) (proj i) s' f :=
by
let id' := ContinuousLinearMap.id 𝕜 (∀ i, F' i)
have h := ((hasFDerivWithinAt_pi' (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (Φ' := id') (x := f) (s := s'))).1
have h' : comp (proj i) id' = proj i := by rfl
rw [← h']; apply h; apply hasFDerivWithinAt_id
