hasStrictDerivAt_finCons' — Mathlib

English

If h : HasStrictDerivAt φ φ' x and hs : HasStrictDerivAt φs φs' x, then HasStrictDerivAt (λ x, Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x.

Русский

Если h и hs заданы как строгие производные частей, то строгая производная Fin.cons образуется из них.

LaTeX

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

Lean4

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

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