left_le_midpoint

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

English

For a < b, lineMap a b r ≤ lineMap a b r' if and only if r ≤ r'.

Русский

Для a < b, lineMap a b r ≤ lineMap a b r' тогда и только тогда, когда r ≤ r'.

LaTeX

$$$a < b \rightarrow (lineMap(a,b;r) \le lineMap(a,b;r') \iff r \le r')$$$

Lean4

@[simp]
theorem left_le_midpoint : a ≤ midpoint k a b ↔ a ≤ b :=
  left_le_lineMap_iff_le <| inv_pos.2 zero_lt_two

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

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

Разделы

Аффилиация

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