lineDeriv_eq_fderiv — Mathlib

English

If the line derivative exists for every direction via the line map, then f is differentiable at x and the line derivative reproduces the differential.

Русский

Если линейная производная существует по каждой линии через x, то f дифференцируема в x, и линейная производная совпадает с дифференциалом.

LaTeX

$$$\text{HasLineDerivAt}_{\mathbb{k}}(f,f',x,v) \Rightarrow f' = fderiv_{\mathbb{k}}(f,x)(v)$$$

Lean4

theorem lineDeriv_eq_fderiv (hf : DifferentiableAt 𝕜 f x) : lineDeriv 𝕜 f x v = fderiv 𝕜 f x v :=
  (hf.hasFDerivAt.hasLineDerivAt v).lineDeriv

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