lt_of_smul_lt_smul_left — Mathlib

English

Let a ≥ 0 act on β by a • b. If a • b1 < a • b2, then b1 < b2, assuming the positivity-reflection property for the scalar action.

Русский

Пусть a ∈ α удовлетворяет a ≥ 0 и действует на β через умножение на скаляр: a • b. Если a • b1 < a • b2, тогда b1 < b2, при условии отражения строгого порядка положительным действием скаляра.

LaTeX

$$$IsOrderedModule\;\alpha\;\alpha \,\rightarrow IsOrderedModule\;\alpha\;\alpha$$$

Lean4

theorem lt_of_smul_lt_smul_left [PosSMulReflectLT α β] (h : a • b₁ < a • b₂) (ha : 0 ≤ a) : b₁ < b₂ :=
  PosSMulReflectLT.lt_of_smul_lt_smul_left ha h

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