one_toPGame_leftMoves_default_eq — Mathlib

English

The default left move for toPGame 1 is the canonical image of 0 under the left-move bijection.

Русский

Стандартный левый ход для toPGame 1 — это каноническое изображение 0 через биекцию левых ходов.

LaTeX

$$$ default : (toPGame 1).LeftMoves = @toLeftMovesToPGame 1 \\langle 0, Set.mem_Iio.mpr zero_lt_one \\rangle.$$$

Lean4

@[simp]
theorem one_toPGame_leftMoves_default_eq :
    (default : (toPGame 1).LeftMoves) = @toLeftMovesToPGame 1 ⟨0, Set.mem_Iio.mpr zero_lt_one⟩ :=
  rfl

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