English
Let f be analytic on univ. For any n and any permutation σ of Fin(n), the domain of the nth iterated derivative is invariant under permuting inputs: (iteratedFDeriv 𝕜 n f x).domDomCongr σ = iteratedFDeriv 𝕜 n f x.
Русский
Пусть f аналитична на всём пространстве. Для любого n и любой перестановки σ на Fin(n) область определения n-й итеративной производной не меняется при перестановке аргументов: (iteratedFDeriv 𝕜 n f x).domDomCongr σ = iteratedFDeriv 𝕜 n f x.
LaTeX
$$$\left(\operatorname{iteratedFDeriv}_{\mathbb{k}}^{(n)} f\right)(x).\mathrm{domDomCongr}\,\sigma = \operatorname{iteratedFDeriv}_{\mathbb{k}}^{(n)} f(x).$$$
Lean4
theorem domDomCongr_iteratedFDeriv (h : AnalyticOn 𝕜 f univ) {n : ℕ} (σ : Perm (Fin n)) :
(iteratedFDeriv 𝕜 n f x).domDomCongr σ = iteratedFDeriv 𝕜 n f x :=
by
rw [← iteratedFDerivWithin_univ]
exact h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _
