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