iteratedPDeriv_one — Mathlib

English

If m is a singleton, iteratedPDeriv reduces to the single directional derivative pderivCLM 𝕜 (m 0).

Русский

Если m состоит из одного направления, то iteratedPDeriv сводится к единственной направленной производной pderivCLM 𝕜 (m 0).

LaTeX

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

Lean4

@[simp]
theorem iteratedPDeriv_one (m : Fin 1 → E) (f : 𝓢(E, F)) : iteratedPDeriv 𝕜 m f = pderivCLM 𝕜 (m 0) f :=
  rfl

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