addRightMono

Mathlib.SetTheory.PGame.Algebra

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.addRightMono

English

If x ≤ y then x + z ≤ y + z for all z.

Русский

Если x ≤ y, то для любого z выполняется x+z ≤ y+z.

LaTeX

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

Lean4

instance addRightMono : AddRightMono PGame :=
  ⟨fun _ _ _ => add_le_add_right'⟩

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

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

Разделы

Аффилиация

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