finCons — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem finCons {φ' : F' 0} {φs' : Π i, F' (Fin.succ i)} {l : Filter 𝕜} (h : HasDerivAtFilter φ φ' x l)
    (hs : HasDerivAtFilter φs φs' x l) : HasDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x l :=
  hasDerivAtFilter_finCons'.mpr ⟨h, hs⟩

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