lineMap_lt_right_iff_lt — Mathlib

English

If a < b, then for any r with 0 < r, we have lineMap a b r < b if and only if a < b.

Русский

Если a < b, то для любого r с 0 < r выполняется lineMap a b r < b тогда и только тогда, когда a < b.

LaTeX

$$$0 < r \rightarrow (\operatorname{lineMap}(a,b;r) < b \iff a < b)$$$

Lean4

theorem lineMap_lt_right_iff_lt (h : r < 1) : lineMap a b r < b ↔ a < b :=
  Iff.trans (by rw [lineMap_apply_one]) (lineMap_lt_lineMap_iff_of_lt h)

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