right_lt_lineMap_iff_lt — Mathlib

English

If r < 1 and a < b, then lineMap a b r < b is equivalent to a < b; equivalently, b > lineMap a b r implies b > a.

Русский

Если r < 1 и a < b, то lineMap a b r < b эквивалентно a < b; эквивалентно, если b > lineMap a b r, то b > a.

LaTeX

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

Lean4

theorem right_lt_lineMap_iff_lt (h : r < 1) : b < lineMap a b r ↔ b < a :=
  lineMap_lt_right_iff_lt (E := Eᵒᵈ) h

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