smul_le_smul_iff_of_pos_left — Mathlib

English

For a > 0, left multiplication by a reflects order: a • b1 ≤ a • b2 iff b1 ≤ b2, under PosSMulMono and PosSMulReflectLE.

Русский

При a > 0 левая операция умножения на скаляр отражает порядок: a • b1 ≤ a • b2 тогда и только тогда, когда b1 ≤ b2, при условии PosSMulMono и PosSMulReflectLE.

LaTeX

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

Lean4

@[simp]
theorem smul_le_smul_iff_of_pos_left [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) :
    a • b₁ ≤ a • b₂ ↔ b₁ ≤ b₂ :=
  ⟨fun h ↦ le_of_smul_le_smul_left h ha, fun h ↦ smul_le_smul_of_nonneg_left h ha.le⟩

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