right_le_lineMap_iff_le

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

English

For a fixed a, b and r, b ≤ lineMap a b r is equivalent to 1 ≤ r when a < b.

Русский

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

LaTeX

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

Lean4

theorem right_le_lineMap_iff_le (h : r < 1) : b ≤ lineMap a b r ↔ b ≤ a :=
  lineMap_le_right_iff_le (E := Eᵒᵈ) h

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

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

Разделы

Аффилиация

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