midpoint_le_right

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

English

For all a, b, the inequality involving midpoint and endpoints respects the order relation.

Русский

Неравенство, содержащее середину и концы, сохраняет порядок.

LaTeX

$$$a \le b \rightarrow (\operatorname{midpoint}(k,a,b) \le b \iff a \le b)$$$

Lean4

@[simp]
theorem midpoint_le_right : midpoint k a b ≤ b ↔ a ≤ b :=
  lineMap_le_right_iff_le two_inv_lt_one

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

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

Разделы

Аффилиация

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