lineMap_le_lineMap_iff_of_lt' — Mathlib

English

If a < b, then for any r, r', lineMap a b r ≤ lineMap a b r' holds if and only if r ≤ r'.

Русский

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

LaTeX

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

Lean4

theorem lineMap_le_lineMap_iff_of_lt' (h : a < b) : lineMap a b r ≤ lineMap a b r' ↔ r ≤ r' :=
  by
  simp only [lineMap_apply_module']
  rw [add_le_add_iff_right, smul_le_smul_iff_of_pos_right (sub_pos.mpr h)]

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