finCons — Mathlib

English

Alternative statement for derivative of Fin.cons via hasDerivWithinAt_finCons'.

Русский

Альтернативное формулирование для производной Fin.cons через hasDerivWithinAt_finCons'.

LaTeX

$$$HasDerivWithinAt\\ φ φ' s x \\land HasDerivWithinAt\\ φs φs' s x\\iff HasDerivWithinAt\\ (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x$$$

Lean4

theorem finCons {φ' : F' 0} {φs' : Π i, F' (Fin.succ i)} (h : HasDerivWithinAt φ φ' s x)
    (hs : HasDerivWithinAt φs φs' s x) : HasDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x :=
  hasDerivWithinAt_finCons'.mpr
    ⟨h, hs⟩
      -- TODO: write the `Fin.cons` versions of `derivWithin_pi` and `deriv_pi`

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