English
Variant: HasFDerivWithinAt (Fin.cons ...) φ'.finCons φs' holds iff HasFDerivWithinAt φ ((π_0) ∘L φ') s x ∧ HasFDerivWithinAt φs (Pi.compRightL 𝕜 F' Fin.succ ∘L φ') s x.
Русский
Условие для внутренней производной в фин-конс.
LaTeX
$$$HasFDerivWithinAt\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi(x),\\phi_s(x))\\big) (\\phi'.finCons\\phi_s') s x \\iff HasFDerivWithinAt\\phi ((\\mathrm{proj}_0) \\circL \\phi') s x ∧ HasFDerivWithinAt\\phi_s (\\Pi.compRightL 𝕜 F' Fin.succ ∘L \\phi') s x$$
Lean4
theorem hasFDerivWithinAt_finCons {φ' : E →L[𝕜] Π i, F' i} :
HasFDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) φ' s x ↔
HasFDerivWithinAt φ (.proj 0 ∘L φ') s x ∧ HasFDerivWithinAt φs (Pi.compRightL 𝕜 F' Fin.succ ∘L φ') s x :=
hasFDerivAtFilter_finCons
