eq — Mathlib · SciLib

English

If IsSymmSndFDerivWithinAt holds, then swapping v,w in the derivative yields equality.

Русский

Если выполняется IsSymmSndFDerivWithinAt, то при перестановке аргументов производной получаем равенство.

LaTeX

$$$\\forall v,w, \\ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v w = fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x w v$$$

Lean4

protected theorem eq (h : IsSymmSndFDerivWithinAt 𝕜 f s x) (v w : E) :
    fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v w = fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x w v :=
  h v w

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