English
The derivative of the Fin-cons map x ↦ Fin.cons(φ(x), φs(x)) at x equals φ'.finCons φs' provided the derivatives of φ and φs exist appropriately.
Русский
Производная от x ↦ Fin.cons(φ(x), φs(x)) равна φ'.finCons φs' при существовании производных φ и φs.
LaTeX
$$$\\HasStrictFDerivAt\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi(x),\\phi_s(x))\\big)\\phi'\\;x \\;\\Longleftrightarrow\\; \\HasStrictFDerivAt\\phi(\\pi_0\\circ\\phi')\\;x \\wedge \\HasStrictFDerivAt\\phi_s\\Big(\\Pi.compRightL 𝕜 F' Fin.succ\\circ\\!\\!L\\phi'\\Big) x$$
Lean4
theorem hasStrictFDerivAt_finCons {φ' : E →L[𝕜] Π i, F' i} :
HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔
HasStrictFDerivAt φ (.proj 0 ∘L φ') x ∧ HasStrictFDerivAt φs (Pi.compRightL 𝕜 F' Fin.succ ∘L φ') x :=
by
rw [hasStrictFDerivAt_pi', Fin.forall_fin_succ, hasStrictFDerivAt_pi']
dsimp [ContinuousLinearMap.comp, LinearMap.comp, Function.comp_def]
simp only [Fin.cons_zero, Fin.cons_succ]
