hasDerivAt_finCons' — Mathlib

English

A simp lemma: Eq (HasDerivAt φ φ' x) (∀ i, HasDerivAt (λ x, φ x i) (φ' i) x).

Русский

Упрощённое лемматическое равенство: HasDerivAt равняется всем координатным производным.

LaTeX

$$$Eq (HasDerivAt φ φ' x) (∀ i, HasDerivAt (\lambda x, φ x i) (φ' i) x)$$$

Lean4

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

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