English
If each α i is an ordered cancellative monoid, then the lexicographic product Lex (∀ i, α i) is an IsOrderedCancelMonoid.
Русский
Если каждый α i — упорядоченный отменимый моноид, то лексикографическое произведение Lex (∀ i, α i) является IsOrderedCancelMonoid.
LaTeX
$$IsOrderedCancelMonoid (Lex (∀ i, α i))$$
Lean4
@[to_additive]
instance isOrderedCancelMonoid [∀ i, CommMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, IsOrderedCancelMonoid (α i)] :
IsOrderedCancelMonoid (Lex (∀ i, α i))
where
mul_le_mul_left _ _ hxy
z :=
hxy.elim (fun hxyz => hxyz ▸ le_rfl) fun ⟨i, hi⟩ =>
Or.inr ⟨i, fun j hji => congr_arg (z j * ·) (hi.1 j hji), mul_lt_mul_left' hi.2 _⟩
le_of_mul_le_mul_left _ _ _
hxyz :=
hxyz.elim (fun h => (mul_left_cancel h).le) fun ⟨i, hi⟩ =>
Or.inr ⟨i, fun j hj => (mul_left_cancel <| hi.1 j hj), lt_of_mul_lt_mul_left' hi.2⟩
