iteratedFDerivWithin_zero_eq — Mathlib

English

The zeroth iterated derivative equals the composition with the inverse curry map: 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).symm \circ f$$$

Lean4

theorem iteratedFDerivWithin_zero_eq : iteratedFDerivWithin 𝕜 0 f s = iteratedFDeriv 𝕜 0 f :=
  rfl

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