grundyValue_eq_iff_equiv — Mathlib

English

For any G, GrundyValue(G) = o iff G ≈ nim(toOrdinal(o)).

Русский

Для любой G, grundyValue(G) = o тогда и только тогда, когда G ≈ nim(toOrdinal(o)).

LaTeX

$$$ \operatorname{grundyValue}(G) = o \iff G \approx \mathrm{nim}(toOrdinal(o)). $$$

Lean4

theorem grundyValue_eq_iff_equiv (G H : PGame) [G.Impartial] [H.Impartial] : grundyValue G = grundyValue H ↔ (G ≈ H) :=
  grundyValue_eq_iff_equiv_nim.trans (equiv_congr_left.1 (equiv_nim_grundyValue H) _).symm

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