left_lt_lineMap_iff_lt — Mathlib

English

Let a, b be elements of an ordered module with a < b. For any r with 0 < r, we have a < lineMap(a, b, r) if and only if a < b.

Русский

Пусть a, b принадлежат упорядочиваемому модулю. При любом r с 0 < r выполняется: a < lineMap(a, b, r) тогда и только тогда, когда a < b.

LaTeX

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

Lean4

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

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