English
The Lexicographic product Lex(α, β) is an ordered monoid when α is a commutative monoid with order and MulLeftStrictMono on α, and β is an ordered monoid.
Русский
Лексикографическое произведение Lex(α, β) — это упорядоченный моноид, когда α — коммутативный моноид с порядком и строгий слева, а β — упорядоченный моноид.
LaTeX
$$IsOrderedMonoid(Lex(α, β))$$
Lean4
@[to_additive]
instance isOrderedMonoid [CommMonoid α] [PartialOrder α] [MulLeftStrictMono α] [CommMonoid β] [PartialOrder β]
[IsOrderedMonoid β] : IsOrderedMonoid (α ×ₗ β) where
mul_le_mul_left _ _ hxy
z :=
(le_iff.1 hxy).elim (fun hxy => left _ _ <| mul_lt_mul_left' hxy _)
(fun hxy => le_iff.2 <| Or.inr ⟨by simp only [ofLex_mul, fst_mul, hxy.1], mul_le_mul_left' hxy.2 _⟩)
