slope_same

Mathlib.LinearAlgebra.AffineSpace.Slope

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

English

The slope of f at identical endpoints equals zero: slope f a a = 0.

Русский

Уклон функции при одинаковых концах равен нулю: slope f a a = 0.

LaTeX

$$$\operatorname{slope}(f,a,a) = 0$$$

Lean4

@[simp]
theorem slope_same (f : k → PE) (a : k) : (slope f a a : E) = 0 := by rw [slope, sub_self, inv_zero, zero_smul]

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

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

Разделы

Аффилиация

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