addRightMono

Mathlib.Data.Finsupp.Lex

URI: https://scilib.ai/kg/mathlib#Finsupp.Lex.addRightMono

English

Lex(α →₀ N) is AddRightMono: adding on the right preserves order.

Русский

Lex(α →₀ N) обладает AddRightMono: добавление справа сохраняет порядок.

LaTeX

$$$\\forall f,g,h,\\ f \\le g \\Rightarrow f+h \\le g+h$$$

Lean4

instance addRightMono : AddRightMono (Lex (α →₀ N)) :=
  addRightMono_of_addRightStrictMono _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru