unique — Mathlib

English

If two line derivatives exist at the same point x in the same direction v for a function f, then they coincide; the line derivative is unique when it exists.

Русский

Если существует две линейные производные одной и той же функции в одной и той же точке и направлении, они совпадают; производная по линии уникальна, когда она существует.

LaTeX

$$$ HasLineDerivAt 𝕜 f f_0' x v \\land HasLineDerivAt 𝕜 f f_1' x v \\Rightarrow f_0' = f_1' $$$

Lean4

theorem unique (h₀ : HasLineDerivAt 𝕜 f f₀' x v) (h₁ : HasLineDerivAt 𝕜 f f₁' x v) : f₀' = f₁' :=
  HasDerivAt.unique h₀ h₁

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