toLex_monotone

Mathlib.Data.Finsupp.Lex

URI: https://scilib.ai/kg/mathlib#Finsupp.toLex_monotone

← MathLib Explorer

English

The map toLex is monotone: if a ≤ b then toLex(a) ≤ toLex(b).

Русский

Функция toLex монотонна: если a ≤ b, то toLex(a) ≤ toLex(b).

LaTeX

$$$\\forall a,b,\\ a \\le b \\Rightarrow \\operatorname{toLex}(a) \\le \\operatorname{toLex}(b)$$$

Lean4

theorem toLex_monotone : Monotone (@toLex (α →₀ N)) := fun a b h ↦
  DFinsupp.toLex_monotone (id h : ∀ i, ofLex (toDFinsupp a) i ≤ ofLex (toDFinsupp b) i)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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