finCons — Mathlib

English

Variant: HasFDerivWithinAt (Fin.cons ...) φ'.finCons φs' is equivalent to HasFDerivWithinAt φ φ' s x ∧ HasFDerivWithinAt φs φs' 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\\phi' s x ∧ HasFDerivWithinAt\\phi_s\\phi_s' s x$$

Lean4

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

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