hasLineDerivAt — Mathlib

English

If f is differentiable at x, then the line derivative equals the evaluation of the derivative as a linear functional on v.

Русский

Если функция дифференцируемa в точке x, то линейная производная вдоль линии равна применению производной к вектору v.

LaTeX

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

Lean4

theorem hasLineDerivAt (hf : HasFDerivAt f L x) (v : E) : HasLineDerivAt 𝕜 f (L v) x v :=
  by
  rw [← hasLineDerivWithinAt_univ]
  exact hf.hasFDerivWithinAt.hasLineDerivWithinAt v

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