lineDeriv — Mathlib

English

If HasLineDerivAt holds for two line derivatives along the same direction at the same point, then the two derivatives coincide.

Русский

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

LaTeX

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

Lean4

protected theorem lineDeriv (h : HasLineDerivAt 𝕜 f f' x v) : lineDeriv 𝕜 f x v = f' := by
  rw [h.unique h.lineDifferentiableAt.hasLineDerivAt]

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