hasDerivWithinAt_finCons' — Mathlib

English

The derivative of Fin.cons is the Fin.cons of derivatives, provided derivatives exist for the components.

Русский

Производная Fin.cons равна Fin.cons производных компонентов, если они существуют.

LaTeX

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

Lean4

/-- A variant of `hasDerivWithinAt_finCons` where the derivative variables are free on the RHS
instead. -/
theorem hasDerivWithinAt_finCons' {φ' : F' 0} {φs' : Π i, F' (Fin.succ i)} :
    HasDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x ↔
      HasDerivWithinAt φ φ' s x ∧ HasDerivWithinAt φs φs' s x :=
  hasDerivAtFilter_finCons

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