addRightMono — Mathlib

English

The lexicographic dependent finitely supported functions form a left-monotone additive structure given compatible per-coordinate addition.

Русский

Лексикографические функции с конечной опорой образуют левостороннюю моноидальную структуру сложения при совместной по всем координатам сложении.

LaTeX

$$$$ \\text{AddLeftMonoid}(\\\\mathrm{Lex}(\\\\Pi_i α_i)) $$$$

Lean4

instance addRightMono : AddRightMono (Lex (Π₀ i, α i)) :=
  addRightMono_of_addRightStrictMono _

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