right_le_midpoint

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

English

For 0 < r (with appropriate a,b) the slope inequality translates to lineMap comparisons.

Русский

Для подходящих a,b и 0 < r наклон переводится в сравнение lineMap.

LaTeX

$$Детерминированное утверждение о наклоне и LineMap$$

Lean4

@[simp]
theorem right_le_midpoint : b ≤ midpoint k a b ↔ b ≤ a :=
  right_le_lineMap_iff_le two_inv_lt_one

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

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

Разделы

Аффилиация

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