slope_sub_smul — Mathlib

English

If a ≠ b, then slope (f) between a and b equals f(b) in terms of slope with line map parameterization: slope (fun x => (x - a) • f x) a b = f b.

Русский

Если a ≠ b, то наклон функции f между a и b равен f(b) для соответствующего преобразования: slope (fun x => (x - a) • f x) a b = f b.

LaTeX

$$$\operatorname{slope}(\lambda x. (x-a)\cdot f(x), a, b) = f(b)$$$

Lean4

@[simp]
theorem slope_sub_smul (f : k → E) {a b : k} (h : a ≠ b) : slope (fun x => (x - a) • f x) a b = f b := by
  simp [slope, inv_smul_smul₀ (sub_ne_zero.2 h.symm)]

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