addLeftMono — Mathlib

English

Addition on the left is monotone with respect to the lexicographic order on dependent finitely supported functions: if x ≤ y, then x + z ≤ y + z for all z.

Русский

Сложение слева монотонно относительно лексикографического порядка на зависимые функции с конечной опорой: если x ≤ y, то x + z ≤ y + z для всех z.

LaTeX

$$$$ x \\le y \\Rightarrow x+z \\le y+z $$$$

Lean4

instance addLeftMono : AddLeftMono (Lex (Π₀ i, α i)) :=
  addLeftMono_of_addLeftStrictMono _

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