rightMovesNimRecOn — Mathlib

English

There is a recursion principle for right moves of a nim game: given a predicate P on right moves, if P holds for all successors coming from right moves of all smaller ordinals, then P holds for any right move.

Русский

Существуют рекурсивные принципы для правых ходов Nim: если свойство выполняется для всех переходов справа, то оно держится для любого правого хода.

LaTeX

$$$ \text{RightMovesNimRecOn}: \forall{o}, \forall P:(\text{nim } o).\text{RightMoves} \to \text{Sort},\; (i:\text{nim } o).\text{RightMoves},\; \left(\forall a

Lean4

/-- A recursion principle for right moves of a nim game. -/
@[elab_as_elim]
def rightMovesNimRecOn {o : Ordinal} {P : (nim o).RightMoves → Sort*} (i : (nim o).RightMoves)
    (H : ∀ a (H : a < o), P <| toRightMovesNim ⟨a, H⟩) : P i := by rw [← toRightMovesNim.apply_symm_apply i]; apply H

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