iteratedPDeriv_succ_left — Mathlib

English

For m : Fin (n+1) → E, iteratedPDeriv 𝕜 m f equals pderivCLM 𝕜 (m 0) applied to iteratedPDeriv 𝕜 (Fin.tail m) f.

Русский

Для m : Fin (n+1) → E имеем iteratedPDeriv 𝕜 m f = pderivCLM 𝕜 (m 0) (iteratedPDeriv 𝕜 (Fin.tail m) f).

LaTeX

$$$iteratedPDeriv 𝕜\, m\, f = pderivCLM 𝕜 (m 0) (iteratedPDeriv 𝕜 (Fin.tail m) f)$$$

Lean4

theorem iteratedPDeriv_succ_left {n : ℕ} (m : Fin (n + 1) → E) (f : 𝓢(E, F)) :
    iteratedPDeriv 𝕜 m f = pderivCLM 𝕜 (m 0) (iteratedPDeriv 𝕜 (Fin.tail m) f) :=
  rfl

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