toSMulPosMono — Mathlib

English

If SMulPosReflectLT holds for α β, then SMulPosMono α β holds: left-multiplication by nonnegative scalars is monotone in the left argument.

Русский

Если SMulPosReflectLT выполняется, то SMulPosMono: левоумножение на неотрицательные скаляры монотонно по левому аргументу.

LaTeX

$$SMulPosReflectLT\\,\\alpha\\,\\beta \\Rightarrow SMulPosMono\\,\\alpha\\,\\beta$$

Lean4

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

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