toPosMulMono — Mathlib

English

If α is equipped with a MulZeroClass and a PartialOrder, and α has PosMulStrictMono, then α has PosMulMono: for every a with a > 0, the map x ↦ a · x is order-preserving.

Русский

Пусть α имеет умножение с нулём и частичный порядок, и если α обладает свойством PosMulStrictMono, то оно обладает PosMulMono: для любого a > 0 отображение x ↦ a · x монотонно по отношению к ≤.

LaTeX

$$$PosMulStrictMono\,\alpha \Rightarrow PosMulMono\,\alpha$$$

Lean4

instance (priority := 100) toPosMulMono [PosMulStrictMono α] : PosMulMono α :=
  posMulMono_iff_covariant_pos.2
    (covariantClass_le_of_lt _ _ _)
      -- see Note [lower instance priority]

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