English
If HasStrictFDerivAt φ φ' x and HasStrictFDerivAt φs φs' x hold, then HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x.
Русский
Если существуют строгие производные φ и φ_s, то существует строгая производная от Fin.cons(φ, φ_s).
LaTeX
$$$\\HasStrictFDerivAt\\phi\\phi' x \\to\\ HasStrictFDerivAt\\phi_s\\phi_s' x \\to \\HasStrictFDerivAt\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi(x),\\phi_s(x))\\big) (\\phi'.\\mathrm{finCons}\\;\\phi_s')x$$
Lean4
/-- A variant of `hasStrictFDerivAt_finCons` where the derivative variables are free on the RHS
instead. -/
theorem hasStrictFDerivAt_finCons' {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] Π i, F' (Fin.succ i)} :
HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x ↔
HasStrictFDerivAt φ φ' x ∧ HasStrictFDerivAt φs φs' x :=
hasStrictFDerivAt_finCons
