hasFDerivAt_finCons — Mathlib

English

Variant: HasFDerivAtFilter (Fin.cons ...) φ'.finCons φs' is equivalent to HasFDerivAtFilter φ φ' x l ∧ HasFDerivAtFilter φs φs' x l.

Русский

Вариант: эквивалентность для HasFDerivAtFilter.

LaTeX

$$$HasFDerivAtFilter\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi(x),\\phi_s(x))\\big) (\\phi'.\\finCons\\phi_s') x l \\iff HasFDerivAtFilter\\phi\\phi' x l \\land HasFDerivAtFilter\\phi_s\\phi_s' x l$$

Lean4

theorem hasFDerivAt_finCons {φ' : E →L[𝕜] Π i, F' i} :
    HasFDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔
      HasFDerivAt φ (.proj 0 ∘L φ') x ∧ HasFDerivAt φs (Pi.compRightL 𝕜 F' Fin.succ ∘L φ') x :=
  hasFDerivAtFilter_finCons

Похожие утверждения