English
A version for HasFDerivAtFilter: if HasFDerivAtFilter φ φ' x l and HasFDerivAtFilter φs φs' x l then HasFDerivAtFilter (λ x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x l.
Русский
Версия для HasFDerivAtFilter: если существуют производные для φ и φ_s в фильтре, то есть производная композиции.
LaTeX
$$$HasFDerivAtFilter\\phi\\phi' x\\;l \\to\\ HasFDerivAtFilter\\phi_s\\phi_s' x\\;l \\to\\ HasFDerivAtFilter\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi x)(\\phi_s x)\\big) (\\phi'.\\finCons\\phi_s') x l$$
Lean4
theorem finCons {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] Π i, F' (Fin.succ i)} {l : Filter E} (h : HasFDerivAtFilter φ φ' x l)
(hs : HasFDerivAtFilter φs φs' x l) : HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x l :=
hasFDerivAtFilter_finCons'.mpr ⟨h, hs⟩
