tensorIteratedFDerivTwo_eq_iteratedFDeriv

English

Equality between tensorIteratedFDerivWithinTwo and iteratedFDerivWithinTwo in tensor form.

Русский

Равенство между tensorIteratedFDerivWithinTwo и iteratedFDerivWithinTwo в тензорной форме.

LaTeX

$$tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin$$

Lean4

/-- Expression of `tensorIteratedFDerivTwo` in terms of `iteratedFDeriv`.
-/
theorem tensorIteratedFDerivTwo_eq_iteratedFDeriv (f : E → F) (e e₁ e₂ : E) :
    tensorIteratedFDerivTwo 𝕜 f e (e₁ ⊗ₜ[𝕜] e₂) = iteratedFDeriv 𝕜 2 f e ![e₁, e₂] := by
  rw [← bilinearIteratedFDerivTwo_eq_iteratedFDeriv, tensorIteratedFDerivTwo, lift.tmul]

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