grundyValue_iff_equiv_zero — Mathlib

English

For impartial G and H, GrundyValue(G) = GrundyValue(H) iff G ≈ H.

Русский

Для беспристрастных G и H, GrundyValue(G) = GrundyValue(H) тогда и только тогда, когда G ≈ H.

LaTeX

$$$ \operatorname{grundyValue}(G) = \operatorname{grundyValue}(H) \iff G \approx H. $$$

Lean4

theorem grundyValue_iff_equiv_zero (G : PGame) [G.Impartial] : grundyValue G = 0 ↔ G ≈ 0 := by
  rw [← grundyValue_eq_iff_equiv, grundyValue_zero]

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