impartial_nim — Mathlib

English

For any ordinal o, Nim(o) is impartial; Nimbers form impartial games.

Русский

Для любого ordinals Nim(o) является беспристрастной игрой; ниберы образуют беспристрастные игры.

LaTeX

$$$ \mathrm{Impartial}(\mathrm{nim}(o)). $$$

Lean4

instance impartial_nim (o : Ordinal) : Impartial (nim o) :=
  by
  induction o using Ordinal.induction with
  | _ o IH
  rw [impartial_def, neg_nim]
  refine ⟨equiv_rfl, fun i => ?_, fun i => ?_⟩ <;> simpa using IH _ (typein_lt_self _)

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