shiftUp

Mathlib.SetTheory.Game.Domineering

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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