iteratedPDeriv_zero — Mathlib

English

If m is the empty index (Fin 0 → E), the iterated partial derivative is the identity on Schwartz space.

Русский

Если m задаёт пустой набор индексов (Fin 0 → E), то итеративная частная производная является тождественным отображением на Schwartz пространство.

LaTeX

$$$iteratedPDeriv 𝕜 m f = f$ при m : Fin 0 → E$$

Lean4

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

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