eq — Mathlib · SciLib

English

IsSymmSndFDerivWithinAt is equivalent to a symmetric condition on iterated derivatives.

Русский

IsSymmSndFDerivWithinAt эквивалентно симметричному условию относительно итерационных производных.

LaTeX

$$$\\text{IsSymmSndFDerivWithinAt}_{\\mathbb{K}}(f,s,x) \\iff (\\text{iteratedFDerivWithin}_{\\mathbb{K}}\\ 2\,f\, s\, x) \\text{ is symmetric under Fin.revPerm}$$$

Lean4

protected theorem eq (h : IsSymmSndFDerivAt 𝕜 f x) (v w : E) :
    fderiv 𝕜 (fderiv 𝕜 f) x v w = fderiv 𝕜 (fderiv 𝕜 f) x w v :=
  h v w

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