iteratedFDerivWithin_succ_apply_left

English

Applying the (n+1)th derivative to a left-currying argument equals the n-th derivative with adjusted arguments.

Русский

Применение (n+1)-й производной к левому каррированию аргументов эквивалентно n-й производной с соответствующими аргументами.

LaTeX

$$$$\text{iteratedFDerivWithin}(\mathbb{k},n+1,f,s)\; = \; (\text{continuousMultilinearCurryLeftEquiv }\mathbb{k} \; (\text{Fin} (n+1) \Rightarrow E)\! ).\text{symm} \circ \text{fderivWithin}(\mathbb{k},\text{iteratedFDerivWithin}(\mathbb{k},n,f,s),s).$$$$

Lean4

theorem iteratedFDerivWithin_succ_apply_left {n : ℕ} (m : Fin (n + 1) → E) :
    (iteratedFDerivWithin 𝕜 (n + 1) f s x : (Fin (n + 1) → E) → F) m =
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x : E → E [×n]→L[𝕜] F) (m 0) (tail m) :=
  rfl

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