toPGame_moveLeft_hEq — Mathlib

English

The left-move structure of o.toPGame is equivalent to the mapping given by toLeftMovesToPGame, i.e., moveLeft is isomorphic to a canonical function on o.

Русский

Структура левого хода в o.toPGame изоморфна отображению, заданному toLeftMovesToPGame.

LaTeX

$$$o.toPGame.moveLeft \\simeq (fun x : o.toType => ((enumIsoToType o).symm x).val.toPGame).$$$

Lean4

@[nolint unusedHavesSuffices]
theorem toPGame_moveLeft_hEq {o : Ordinal} :
    o.toPGame.moveLeft ≍ fun x : o.toType => ((enumIsoToType o).symm x).val.toPGame :=
  by
  rw [toPGame]
  rfl

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