finCons — Mathlib

English

Equivalence: HasStrictDerivAt (λ x, Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x holds iff HasStrictDerivAt φ φ' x ∧ HasStrictDerivAt φs φs' x.

Русский

Эквивалентность: строгая производная Fin.cons равна при разложении на φ и φs, если соответствующие строгие производные существуют.

LaTeX

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

Lean4

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

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