addRightStrictMono

Mathlib.Data.DFinsupp.Lex

URI: https://scilib.ai/kg/mathlib#DFinsupp.Lex.addRightStrictMono

← MathLib Explorer

English

If x < y in the lexicographic order, then x + z < y + z for all z.

Русский

Если x < y в лексикографическом порядке, то x + z < y + z для всех z.

LaTeX

$$$$ x < y \\Rightarrow x+z < y+z $$$$

Lean4

instance addRightStrictMono : AddRightStrictMono (Lex (Π₀ i, α i)) :=
  ⟨fun f _ _ ⟨a, lta, ha⟩ ↦ ⟨a, fun j ja ↦ congr_arg (· + ofLex f j) (lta j ja), add_lt_add_right ha _⟩⟩

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

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

Разделы

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

Аффилиация

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