toMulPosMono — Mathlib

English

If α has MulZeroClass and PartialOrder and MulPosStrictMono, then MulPosMono α holds: left multiplication by a positive element is order-preserving.

Русский

Пусть α обладает MulZeroClass и PartialOrder и MulPosStrictMono; тогда MulPosMono выполняется: умножение слева на положительное число сохраняет порядок.

LaTeX

$$$MulPosStrictMono\,\alpha \Rightarrow MulPosMono\,\alpha$$$

Lean4

instance (priority := 100) toMulPosMono [MulPosStrictMono α] : MulPosMono α :=
  mulPosMono_iff_covariant_pos.2
    (covariantClass_le_of_lt _ _ _)
      -- see Note [lower instance priority]

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