leftMovesNimRecOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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