shiftRight

Mathlib.SetTheory.Game.Domineering

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

English

The equivalence shiftRight maps (x, y) to (x+1, y).

Русский

Эквивалент shiftRight преобразует (x, y) в (x+1, y).

LaTeX

$$$\text{shiftRight}: \mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} \times \mathbb{Z},\quad \text{shiftRight}(a,b)=(a+1,b)$$$

Lean4

/-- The equivalence `(x, y) ↦ (x+1, y)`. -/
@[simps!]
def shiftRight : ℤ × ℤ ≃ ℤ × ℤ :=
  (Equiv.addRight (1 : ℤ)).prodCongr (Equiv.refl ℤ)

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

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

Разделы

Аффилиация

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