English
WithinAt variant: the derivative of Fin.cons is the Fin.cons derivative when restricted to s.
Русский
Внутренний вариант: производная от Fin.cons на s равна соответствующей производной.
LaTeX
$$$HasFDerivWithinAt\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi(x),\\phi_s(x))\\big) (\\phi'.finCons\\phi_s') s x \\iff HasFDerivWithinAt\\phi\\phi' s x ∧ HasFDerivWithinAt\\phi_s\\phi_s' s x$$
Lean4
/-- A variant of `hasFDerivAt_finCons` where the derivative variables are free on the RHS
instead. -/
theorem hasFDerivAt_finCons' {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] Π i, F' (Fin.succ i)} :
HasFDerivAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x ↔ HasFDerivAt φ φ' x ∧ HasFDerivAt φs φs' x :=
hasFDerivAt_finCons
