English
The family powHalf is defined recursively by powHalf(0) = 1 and powHalf(n+1) = {0 | powHalf(n)} for all n ∈ ℕ, describing explicit expressions of powers of 1/2 as pre-games.
Русский
Семейство powHalf задаётся рекурсивно: powHalf(0) = 1 и powHalf(n+1) = {0 | powHalf(n)} для всех натуральных n, задающее явные выражения степеней 1/2 как предигры.
LaTeX
$$$\text{powHalf}(0) = 1, \quad \text{powHalf}(n+1) = \{0 \mid \text{powHalf}(n)\}.$$$
Lean4
/-- For a natural number `n`, the pre-game `powHalf (n + 1)` is recursively defined as
`{0 | powHalf n}`. These are the explicit expressions of powers of `1 / 2`. By definition, we have
`powHalf 0 = 1` and `powHalf 1 ≈ 1 / 2` and we prove later on that
`powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n`. -/
def powHalf : ℕ → PGame
| 0 => 1
| n + 1 => ⟨PUnit, PUnit, 0, fun _ => powHalf n⟩
