slope_fun_def

Mathlib.LinearAlgebra.AffineSpace.Slope

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

English

The slope of f on [a,b] can be written uniformly as the function of a and b: slope f = (b−a)^{-1}•(f b − f a).

Русский

Уклон функции f на [a,b] задаётся единицей (b−a)^{-1} и разностью f(b)−f(a).

LaTeX

$$$\operatorname{slope} f = \lambda a b. (b-a)^{-1} \cdot (f(b) -\!\!\!\!\!_v f(a))$$$

Lean4

theorem slope_fun_def (f : k → PE) : slope f = fun a b => (b - a)⁻¹ • (f b -ᵥ f a) :=
  rfl

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

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

Разделы

Аффилиация

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