to_leftMoves_one_toPGame_symm — Mathlib

English

The inverse of the left-move bijection for 1 maps the unique left move back to 0.

Русский

Обратная к биекции левых ходов для 1 отображает единственный левый ход обратно к нулю.

LaTeX

$$$@toLeftMovesToPGame 1)^{-1}(\\text{the unique left move}) = 0.$$$

Lean4

@[simp]
theorem to_leftMoves_one_toPGame_symm (i) : (@toLeftMovesToPGame 1).symm i = ⟨0, Set.mem_Iio.mpr zero_lt_one⟩ := by
  simp [eq_iff_true_of_subsingleton]

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