English
A variant that the Frechét derivative on the RHS is free; HasStrictFDerivAt (Fin.cons...) φ'.finCons φs' is equivalent to HasStrictFDerivAt φ φ' ∧ HasStrictFDerivAt φs φs'.
Русский
Вариант, где правая часть производной свободна; эквивалентно наличие строгих производных φ и φ_s.
LaTeX
$$$HasStrictFDerivAt\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi(x),\\phi_s(x))\\big) (\\phi'.\\finCons\\;\\phi_s') x \\iff HasStrictFDerivAt\\phi\\phi' x \\land HasStrictFDerivAt\\phi_s\\phi_s' x$$
Lean4
@[fun_prop]
theorem finCons {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] Π i, F' (Fin.succ i)} (h : HasStrictFDerivAt φ φ' x)
(hs : HasStrictFDerivAt φs φs' x) : HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x :=
hasStrictFDerivAt_finCons'.mpr ⟨h, hs⟩
