English
For a map Φ: E → ∀ i, F'i, the differentiability (or strict differentiability) of Φ at x with derivative Φ′ is equivalent to differentiability of each coordinate Φ(x) i with derivative ((proj i) ∘ Φ′).
Русский
Для отображения Φ: E → ∀ i, F'i градационная \(x\) сопряжена с дифференцируемостью по каждой координате: Φ(x) i дифференцируемо с производной ((proj i) ∘ Φ′).
LaTeX
$$$\\text{HasStrictFDerivAt } \\ Φ \\ Φ' \\ x \\iff \\forall i, \\ HasStrictFDerivAt(\\, fun x \\mapsto Φ(x)_i \\,) ((proj_i) \\circ Φ') \\ x.$$$
Lean4
@[simp]
theorem hasStrictFDerivAt_pi' :
HasStrictFDerivAt Φ Φ' x ↔ ∀ i, HasStrictFDerivAt (fun x => Φ x i) ((proj i).comp Φ') x :=
by
simp only [hasStrictFDerivAt_iff_isLittleO]
exact isLittleO_pi
