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