lineMap_lt_lineMap_iff_of_lt — Mathlib

English

If a < a', b < b', and 0 ≤ r ≤ 1, then lineMap(a,b,r) < lineMap(a',b',r).

Русский

Если a < a', b < b' и 0 ≤ r ≤ 1, тогда lineMap(a,b,r) < lineMap(a',b',r).

LaTeX

$$$ a < a' \land b < b' \land 0 \le r \land r \le 1 \Rightarrow lineMap(a,b,r) < lineMap(a',b',r) $$$

Lean4

theorem lineMap_lt_lineMap_iff_of_lt (h : r < r') : lineMap a b r < lineMap a b r' ↔ a < b :=
  by
  simp only [lineMap_apply_module]
  rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul, sub_sub_sub_cancel_left,
    smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]

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