toPosSMulMono — Mathlib

English

If left-scalar multiplication reflects LT (PosSMulReflectLT), then left-multiplication is monotone in the second argument (PosSMulMono).

Русский

Если отражение LT слева выполняется (PosSMulReflectLT), то умножение слева является монотонным в правом аргументе (PosSMulMono).

LaTeX

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

Lean4

theorem toPosSMulMono [PosSMulReflectLT α β] : PosSMulMono α β where
  smul_le_smul_of_nonneg_left _a ha _b₁ _b₂ hb := not_lt.1 fun h ↦ hb.not_gt <| lt_of_smul_lt_smul_left h ha

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