English
The slope f a b is a linear combination of slopes f a b and f b c to yield slope f a c with coefficients (b−a)/(c−a) and (c−b)/(c−a).
Русский
Уклон f от a до c выражается линейной комбинацией наклонов f от a до b и f от b до c с коэффициентами (b−a)/(c−a) и (c−b)/(c−a).
LaTeX
$$$\\left(\\frac{b-a}{c-a}\\right) \\cdot \\operatorname{slope} f a b \;+\;\\left(\\frac{c-b}{c-a}\\right) \\cdot \\operatorname{slope} f b c = \\operatorname{slope} f a c$$$
Lean4
@[simp]
theorem sub_smul_slope (f : k → PE) (a b : k) : (b - a) • slope f a b = f b -ᵥ f a :=
by
rcases eq_or_ne a b with (rfl | hne)
· rw [sub_self, zero_smul, vsub_self]
· rw [slope, smul_inv_smul₀ (sub_ne_zero.2 hne.symm)]
