relabelRelabelling — Mathlib

English

Relabelling of a game is Relabelling-equivalent to the original game; i.e., x is Relabelling-equivalent to relabel el er. This demonstrates that relabelling does not change the underlying game up to relabelling.

Русский

Релятабеллинг игры эквивалентен ей самой через Relabelling; то есть x ≃r relabel el er.

LaTeX

$$$ x \\equiv_r \\mathrm{relabel}(el,er). $$$

Lean4

/-- The game obtained by relabelling the next moves is a relabelling of the original game. -/
def relabelRelabelling {x : PGame} {xl' xr'} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves) : x ≡r relabel el er :=
  -- Porting note: needed to add `rfl`

  Relabelling.mk' el er (fun i => by simp; rfl) (fun j => by simp; rfl)

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