hasDerivAt_finCons — Mathlib

English

Variant: HasDerivWithinAt (λ x, Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x iff HasDerivWithinAt φ φ' s x ∧ HasDerivWithinAt φs φs' s x.

Русский

Вариант: HasDerivWithinAt через Fin.cons распадается на производные частей.

LaTeX

$$$HasDerivWithinAt (\lambda x, Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x \iff HasDerivWithinAt φ φ' s x ∧ HasDerivWithinAt φs φs' s x$$$

Lean4

theorem hasDerivAt_finCons {φ' : Π i, F' i} :
    HasDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔ HasDerivAt φ (φ' 0) x ∧ HasDerivAt φs (fun i => φ' i.succ) x :=
  hasDerivAtFilter_finCons

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