slope_def_module

Mathlib.LinearAlgebra.AffineSpace.Slope

URI: https://scilib.ai/kg/mathlib#slope_def_module

English

The slope of a function f at two points a and b is (b−a)^{-1} · (f(b) − f(a)).

Русский

Наклон функции f между точками a и b равен (b−a)^{-1} · (f(b) − f(a)).

LaTeX

$$$\mathrm{slope}(f,a,b) = (b-a)^{-1} \cdot (f(b)-f(a))$$$

Lean4

theorem slope_def_module (f : k → E) (a b : k) : slope f a b = (b - a)⁻¹ • (f b - f a) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru