toSMulPosReflectLT — Mathlib

English

If PosSMulReflectLT holds, then PosSMulMono holds: left-multiplication by nonnegative scalars is monotone in the left argument.

Русский

Если PosSMulReflectLT держится, то PosSMulMono держится: левая монотонность умножения на неотрицательные скаляры.

LaTeX

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

Lean4

theorem toSMulPosReflectLT [SMulPosMono α β] : SMulPosReflectLT α β where
  lt_of_smul_lt_smul_right _b hb _a₁ _a₂ h := not_le.1 fun ha ↦ h.not_ge <| smul_le_smul_of_nonneg_right ha hb

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