isEmpty_nat_rightMoves — Mathlib

English

For every natural number n, the set of right moves of the game n is empty; i.e., RightMoves(n) is empty for all n.

Русский

Для каждого натурального числа n множество правых ходов игры n пусто; RightMoves(n) пусто для всех n.

LaTeX

$$$ \forall n \in \mathbb{N},\; IsEmpty\big(RightMoves(n)\big) $$$

Lean4

instance isEmpty_nat_rightMoves : ∀ n : ℕ, IsEmpty (RightMoves n)
  | 0 => inferInstanceAs (IsEmpty PEmpty)
  | n + 1 => by
    haveI := isEmpty_nat_rightMoves n
    rw [PGame.nat_succ, rightMoves_add]
    infer_instance

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