hasStrictFDerivAt — Mathlib

English

There exists a strict Fréchet derivative for φ.prodFun with a provided derivative mapping φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ..., and φ.pt.

Русский

Существует строгий предел Фреше для φ.prodFun с заданной производной соответствия

LaTeX

$$HasStrictFDerivAt φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv φ.left_range φ.right_range φ.isCompl_ker) φ.pt$$

Lean4

protected theorem hasStrictFDerivAt :
    HasStrictFDerivAt φ.prodFun
      (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv φ.left_range φ.right_range φ.isCompl_ker : E →L[𝕜] F × G)
      φ.pt :=
  φ.left_has_deriv.prodMk φ.right_has_deriv

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