English
The Lex family of dependent finitely supported functions forms an IsOrderedCancelAddMonoid: addition is ordered-cancelative on the left, and cancellation holds from left-leq.
Русский
Семейство лексикографических зависимых функций с конечной опорой образует IsOrderedCancelAddMonoid: слева строгая монотонность и отмена сохраняются слева.
LaTeX
$$$$ \\text{IsOrderedCancelAddMonoid}(\\\\mathrm{Lex}(\\\\Pi_i α_i)) $$$$
Lean4
instance isOrderedCancelAddMonoid [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)]
[∀ i, IsOrderedCancelAddMonoid (α i)] : IsOrderedCancelAddMonoid (Lex (Π₀ i, α i))
where
add_le_add_left _ _ h _ := add_le_add_left (α := Lex (∀ i, α i)) h _
le_of_add_le_add_left _ _ _ := le_of_add_le_add_left (α := Lex (∀ i, α i))
