English
Let h be ContDiffAt 𝕜 ω f x. Then for every permutation σ of Fin(n), the domain-conjugation of the nth iterated derivative equals the derivative itself: (iteratedFDeriv 𝕜 n f x).domDomCongr σ = iteratedFDeriv 𝕜 n f x.
Русский
Пусть h = ContDiffAt 𝕜 ω f x. Тогда для любой перестановки σ на Fin(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 : ContDiffAt 𝕜 ω f x) {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) _
