instIsOrderedSMulOfIsOrderedMonoid

English

In an ordered monoid G, the action by multiplication on itself is order-preserving in both arguments: a ≤ b implies a c ≤ b c and c ≤ d implies a c ≤ a d for all a,b,c,d ∈ G.

Русский

В упорядоченном моноиде G умножение на себя сохраняет порядок в обе стороны: a ≤ b ⇒ a c ≤ b c и c ≤ d ⇒ a c ≤ a d для всех a,b,c,d ∈ G.

LaTeX

$$∀ a,b,c,d ∈ G, a ≤ b ⇒ c ≤ d ⇒ a c ≤ b d$$

Lean4

@[to_additive]
instance [CommMonoid G] [PartialOrder G] [IsOrderedMonoid G] : IsOrderedSMul G G
    where
  smul_le_smul_left _ _ := mul_le_mul_left'
  smul_le_smul_right _ _ := mul_le_mul_right'

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