hasDerivAtFilter_finCons — Mathlib

English

Let φ, φs be functions with HasDerivAtFilter at x with φ' and φs', then HasDerivAtFilter (λ x, Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x l.

Русский

Пусть φ, φs имеют производные по HasDerivAtFilter в x; тогда HasDerivAtFilter для объединённой структуры Fin.cons образуется из их производных.

LaTeX

$$$HasDerivAtFilter (\lambda x, Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x l$$$

Lean4

theorem hasDerivAtFilter_finCons {φ' : Π i, F' i} {l : Filter 𝕜} :
    HasDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) φ' x l ↔
      HasDerivAtFilter φ (φ' 0) x l ∧ HasDerivAtFilter φs (fun i => φ' i.succ) x l :=
  hasFDerivAtFilter_finCons

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