hasDerivWithinAt_finCons — Mathlib

English

Variant: HasDerivWithinAt (λ x, Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x iff both HasDerivWithinAt φ φ' s x and 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 hasDerivWithinAt_finCons {φ' : Π i, F' i} :
    HasDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) φ' s x ↔
      HasDerivWithinAt φ (φ' 0) s x ∧ HasDerivWithinAt φs (fun i => φ' i.succ) s x :=
  hasDerivAtFilter_finCons

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