finCons — Mathlib

English

If HasFDerivAt φ φ' x and HasFDerivAt φs φs' x then HasFDerivAt (λ x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x.

Русский

Если есть производная φ и φ_s в точке x, то есть производная от Fin.cons.

LaTeX

$$$HasFDerivAt\\phi\\phi' x ∧ HasFDerivAt\\phi_s\\phi_s' x \\Rightarrow HasFDerivAt\\big(\\lambda x.\\mathrm{Fin.cons}(\\phi x)(\\phi_s x)\\big) (\\phi'.finCons φs') x$$

Lean4

@[fun_prop]
theorem finCons {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] Π i, F' (Fin.succ i)} (h : HasFDerivWithinAt φ φ' s x)
    (hs : HasFDerivWithinAt φs φs' s x) : HasFDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') s x :=
  hasFDerivWithinAt_finCons'.mpr ⟨h, hs⟩

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