left_le_lineMap_iff_le

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

English

For a fixed a, b and r, if 0 < r then a ≤ lineMap a b r is equivalent to a ≤ b.

Русский

Для фиксированных a, b и r, если 0 < r, то a ≤ lineMap a b r эквивалентно a ≤ b.

LaTeX

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

Lean4

theorem left_le_lineMap_iff_le (h : 0 < r) : a ≤ lineMap a b r ↔ a ≤ b :=
  Iff.trans (by rw [lineMap_apply_zero]) (lineMap_le_lineMap_iff_of_lt h)

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

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

Разделы

Аффилиация

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