impartial_def — Mathlib

English

Let G be a PGame. Then G is impartial if and only if G is equivalent to its negation and every left and right move yields an impartial game.

Русский

Пусть G — игра PGame. Тогда G непредвзята ⇔ G эквивалентна своему отрицанию и каждый левый и правый ход ведут к непредвзятым играм.

LaTeX

$$$\operatorname{Impartial}(G) \iff G \cong -G \land (\forall i, \operatorname{Impartial}(G.moveLeft(i))) \land (\forall j, \operatorname{Impartial}(G.moveRight(j)))$$$

Lean4

theorem impartial_def {G : PGame} :
    G.Impartial ↔ G ≈ -G ∧ (∀ i, Impartial (G.moveLeft i)) ∧ ∀ j, Impartial (G.moveRight j) :=
  by
  simp_rw [impartial_iff_aux]
  rw [ImpartialAux]

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