English
Equivalence: HasDerivWithinAt (λ x, Fin.cons (φ x) (φs x)) φ' s x iff HasDerivWithinAt φ (φ' 0) s x ∧ HasDerivWithinAt φs (λ i, φ' i.succ) s x.
Русский
Эквивалентность: строгая производная через Fin.cons внутри s равна паре производных частей.
LaTeX
$$$HasDerivWithinAt (\lambda x, Fin.cons (φ x) (φs x)) φ' s x \iff HasDerivWithinAt φ (φ' 0) s x ∧ HasDerivWithinAt φs (\lambda i, φ' i.succ) s x$$$
Lean4
/-- A variant of `hasDerivAtFilter_finCons` where the derivative variables are free on the RHS
instead. -/
theorem hasDerivAtFilter_finCons' {φ' : F' 0} {φs' : Π i, F' (Fin.succ i)} {l : Filter 𝕜} :
HasDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x l ↔
HasDerivAtFilter φ φ' x l ∧ HasDerivAtFilter φs φs' x l :=
hasDerivAtFilter_finCons
