addLeftMono

Mathlib.Data.Finsupp.Lex

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

English

Lex(α →₀ N) has AddLeftMono: adding on the left preserves order (not necessarily strictly).

Русский

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

LaTeX

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

Lean4

instance addLeftMono : AddLeftMono (Lex (α →₀ N)) :=
  addLeftMono_of_addLeftStrictMono _

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

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

Разделы

Аффилиация

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