instIsOrderedMonoid — Mathlib

English

The Cartesian product α × β of two ordered monoids is an ordered monoid with the componentwise order.

Русский

Декартово произведение α × β двух упорядоченных моноидов образует упорядоченный моноид с попарно-компонентным порядком.

LaTeX

$$IsOrderedMonoid(\alpha \times \beta)$$

Lean4

@[to_additive]
instance [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CommMonoid β] [PartialOrder β] [IsOrderedMonoid β] :
    IsOrderedMonoid (α × β) where mul_le_mul_left _ _ h _ := ⟨mul_le_mul_left' h.1 _, mul_le_mul_left' h.2 _⟩

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