unique — Mathlib

English

If HasGradientAt f gradf x and HasGradientAt f gradg x then gradf = gradg.

Русский

Если градиент f в x существует как gradf и gradg, то gradf = gradg.

LaTeX

$$$ HasGradientAt\\ f\\ gradf\\ x \\to HasGradientAt\\ f\\ gradg\\ x \\Rightarrow gradf = gradg $$$

Lean4

theorem unique {gradf gradg : F} (hf : HasGradientAt f gradf x) (hg : HasGradientAt f gradg x) : gradf = gradg :=
  (toDual 𝕜 F).injective (hf.hasFDerivAt.unique hg.hasFDerivAt)

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