slope_comm

Mathlib.LinearAlgebra.AffineSpace.Slope

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

← MathLib Explorer

English

The slope is symmetric in the endpoints: slope f a b = slope f b a.

Русский

Уклон симметричен концам: slope f a b = slope f b a.

LaTeX

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

Lean4

theorem slope_comm (f : k → PE) (a b : k) : slope f a b = slope f b a := by
  rw [slope, slope, ← neg_vsub_eq_vsub_rev, smul_neg, ← neg_smul, neg_inv, neg_sub]

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

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

Разделы

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

Аффилиация

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