quot_natCast — Mathlib

English

For every natural number n, the image of n as a PGame, viewed as a Game, equals n as a Game.

Русский

Для каждого натурального числа n образ n как PGame, рассматриваемый как Game, равен n как игре.

LaTeX

$$$ \forall n \in \mathbb{N}, \llbracket n : \mathrm{PGame} \rrbracket = (n : \mathrm{Game}) $$$

Lean4

@[simp]
theorem quot_natCast : ∀ n : ℕ, ⟦(n : PGame)⟧ = (n : Game)
  | 0 => rfl
  | n + 1 => by
    rw [PGame.nat_succ, quot_add, Nat.cast_add, Nat.cast_one, quot_natCast]
    rfl

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