fderivWithin_iteratedFDerivWithin

English

The derivative within a set of an iterated derivative equals the composition with a left curry map.

Русский

Производная внутри множества от идущей последовательности производных эквивалентна композиции с левой каррирующей картой.

LaTeX

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

Lean4

theorem fderivWithin_iteratedFDerivWithin {s : Set E} {n : ℕ} :
    fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s =
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F) ∘ iteratedFDerivWithin 𝕜 (n + 1) f s :=
  rfl

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