English
Variant statement for HasStrictFDerivAt with primed RHS; HasStrictFDerivAt (Fin.cons ...) φ'.finCons φs' is equivalent to HasStrictFDerivAt φ φ' x ∧ HasStrictFDerivAt φs φs' x.
Русский
Вариант для правая часть: эквивалентность строгой производной.
LaTeX
$$$HasStrictFDerivAt\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi(x),\\phi_s(x))\\big) (\\phi'.\\finCons\\phi_s') x \\iff HasStrictFDerivAt\\phi\\phi' x \\land HasStrictFDerivAt\\phi_s\\phi_s' x$$
Lean4
theorem hasFDerivAtFilter_finCons {φ' : E →L[𝕜] Π i, F' i} {l : Filter E} :
HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) φ' x l ↔
HasFDerivAtFilter φ (.proj 0 ∘L φ') x l ∧ HasFDerivAtFilter φs (Pi.compRightL 𝕜 F' Fin.succ ∘L φ') x l :=
by
rw [hasFDerivAtFilter_pi', Fin.forall_fin_succ, hasFDerivAtFilter_pi']
dsimp [ContinuousLinearMap.comp, LinearMap.comp, Function.comp_def]
simp only [Fin.cons_zero, Fin.cons_succ]
