iteratedFDerivWithin_zero_eq_comp

English

iteratedFDerivWithin 0 f s equals the inverse curry of f composed with f.

Русский

iteratedFDerivWithin 0 f s равен композиции с обратной раскладкой и f.

LaTeX

$$$$\text{iteratedFDerivWithin}(\mathbb{k},0,f,s) = (\text{continuousMultilinearCurryFin0 }\mathbb{k} E F)^{-1} \circ f.$$$$

Lean4

theorem iteratedFDerivWithin_zero_eq_comp :
    iteratedFDerivWithin 𝕜 0 f s = (continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f :=
  rfl

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