lineDeriv_zero_of_not_lineDifferentiableAt

English

If the line derivative is not defined (i.e., the function is not linearly differentiable at x in the direction v), then the line derivative in that direction is zero.

Русский

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

LaTeX

$$$\\\\neg \\\\ LineDifferentiableAt 𝕜 f x v \\\\Rightarrow lineDeriv 𝕜 f x v = 0$$$

Lean4

theorem lineDeriv_zero_of_not_lineDifferentiableAt (h : ¬LineDifferentiableAt 𝕜 f x v) : lineDeriv 𝕜 f x v = 0 :=
  deriv_zero_of_not_differentiableAt h

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