hasStrictDerivAt_finCons — Mathlib

English

The derivative of a finite-cons structure Fin.cons (φ x) (φs x) is (φ' , φs') provided φ, φs have derivatives φ', φs' at x.

Русский

Производная структуры Fin.cons состоит из производных частей: если φ имеет производную φ' и φs имеет производную φs' в x, то производная Fin.cons (φ x) (φs x) равна Fin.cons φ' φs'.

LaTeX

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

Lean4

theorem hasStrictDerivAt_finCons {φ' : Π i, F' i} :
    HasStrictDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔
      HasStrictDerivAt φ (φ' 0) x ∧ HasStrictDerivAt φs (fun i => φ' i.succ) x :=
  hasStrictFDerivAt_finCons

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