toPosSMulMono — Mathlib

English

On any ordered semiring α, multiplication defines a positive monotone action of α on itself: a nonnegative scalar multiplies elements with preserved order.

Русский

На упорядоченном полукольце α умножение образует положительную монотонную дею на самом себе: неотрицательное скаляра сохраняет порядок при умножении на элементы.

LaTeX

$$$\\mathrm{PosSMulMono}(\\alpha, \\alpha).$$$

Lean4

instance (priority := 100) toPosSMulMono [PosMulMono α] : PosSMulMono α α where
  smul_le_smul_of_nonneg_left _a ha _b₁ _b₂ hb := mul_le_mul_of_nonneg_left hb ha

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