iteratedFDeriv_cons — Mathlib

English

From symmetry of the IsSymmSndFDerivWithinAt, deduce symmetry of iteratedFDerivWithin.

Русский

Из симметрии IsSymmSndFDerivWithinAt следует симметричность iteratedFDerivWithin.

LaTeX

$$$hf : IsSymmSndFDerivWithinAt 𝕜 f s x \\Rightarrow Iterated symmetry on 2nd derivative within$$$

Lean4

theorem iteratedFDeriv_cons {x v w : E} {hf : IsSymmSndFDerivAt 𝕜 f x} :
    iteratedFDeriv 𝕜 2 f x ![v, w] = iteratedFDeriv 𝕜 2 f x ![w, v] :=
  by
  simp only [← isSymmSndFDerivWithinAt_univ, ← iteratedFDerivWithin_univ] at *
  exact hf.iteratedFDerivWithin_cons uniqueDiffOn_univ (mem_univ _)

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