toPosSMulReflectLT — Mathlib

English

If scalar multiplication by a nonnegative element acts monotonically on the second factor, then it reflects strict order: for all a ≥ 0 and b1, b2 in β, a · b1 < a · b2 implies b1 < b2.

Русский

Если умножение на неотрицательный скаляр действует монотонно на второй фактор, то отражает строгое порядок: для любого a ≥ 0 и b1, b2 ∈ β, если a·b1 < a·b2, то b1 < b2.

LaTeX

$$$PosSMulMono\\,\\alpha\\,\\beta \\Rightarrow PosSMulReflectLT\\,\\alpha\\,\\beta$$$

Lean4

instance toPosSMulReflectLT [PosSMulMono α β] : PosSMulReflectLT α β where
  lt_of_smul_lt_smul_left _a ha _b₁ _b₂ := (monotone_smul_left_of_nonneg ha).reflect_lt

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