iteratedFDeriv_zero_eq_comp — Mathlib

English

The zeroth iterated derivative equals the composition with the inverse curry: iteratedFDeriv 𝕜 0 f = (continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f.

Русский

Нулевая производная равна композиции с обратной карри: iteratedFDeriv 𝕜 0 f = (continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f.

LaTeX

$$$\operatorname{iteratedFDeriv}_{\mathbb{K}}^{0} f = (\text{continuousMultilinearCurryFin0 } 𝕜 E F)^{-1} \circ f$$$

Lean4

theorem iteratedFDeriv_zero_eq_comp : iteratedFDeriv 𝕜 0 f = (continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f :=
  rfl

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