lineDeriv_neg — Mathlib

English

The line derivative is odd in the direction: lineDeriv 𝕜 f x (−v) = − lineDeriv 𝕜 f x v.

Русский

Линейная производная по направлению обратно пропорциональна направлению: lineDeriv 𝕜 f x (−v) = − lineDeriv 𝕜 f x v.

LaTeX

$$$$ lineDeriv 𝕜 f x (-v) = -\, lineDeriv 𝕜 f x v $$$$

Lean4

theorem lineDeriv_neg : lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x v := by
  rw [← neg_one_smul (R := 𝕜) v, lineDeriv_smul, neg_one_smul]

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