smul_lt_smul_iff_of_pos_left — Mathlib

English

With PosSMulStrictMono and PosSMulReflectLT, for a > 0, a • b1 < a • b2 iff b1 < b2.

Русский

При PosSMulStrictMono и PosSMulReflectLT, для a > 0: a • b1 < a • b2 тогда и только тогда, когда b1 < b2.

LaTeX

$$$IsOrderedModule\;\alpha\;β \;(0 < a) \rightarrow (a \cdot b_1 < a \cdot b_2 \iff b_1 < b_2)$$$

Lean4

@[simp]
theorem smul_lt_smul_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
    a • b₁ < a • b₂ ↔ b₁ < b₂ :=
  ⟨fun h ↦ lt_of_smul_lt_smul_left h ha.le, fun hb ↦ smul_lt_smul_of_pos_left hb ha⟩

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