slope_neg — Mathlib

English

If you negate the target function, the slope negates: slope (−f) x y = − slope f x y.

Русский

Если отрицать значение функции, наклон также меняется на противоположный: slope (−f) x y = − slope f x y.

LaTeX

$$$\operatorname{slope}(\lambda t. -f(t))\ x\ y = -\operatorname{slope}(f)\ x\ y$$$

Lean4

@[simp]
theorem slope_neg (f : k → E) (x y : k) : slope (fun t ↦ -f t) x y = -slope f x y := by
  simp only [slope_def_module, neg_sub_neg, ← smul_neg, neg_sub]

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