eq_of_slope_eq_zero

Mathlib.LinearAlgebra.AffineSpace.Slope

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

← MathLib Explorer

English

If the slope between f at a and b is zero, then f(a) = f(b).

Русский

Если наклон между f(a) и f(b) равен нулю, то значения совпадают: f(a)=f(b).

LaTeX

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

Lean4

theorem eq_of_slope_eq_zero {f : k → PE} {a b : k} (h : slope f a b = (0 : E)) : f a = f b := by
  rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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