hyperoperation_ge_four_zero — Mathlib

English

For all n,k ∈ ℕ, H_{n+4}(0,k) equals 1 if k is even and 0 if k is odd.

Русский

Пусть n,k ∈ ℕ. Гипероперация ранга n+4 над 0 и k равна 1, если k чётно, и 0, если нечётно.

LaTeX

$$$\\forall n,k \\in \\mathbb{N}, \\ H_{n+4}(0,k) = \\begin{cases}1, & k \\text{even} \\cr 0, & k \\text{odd} \\end{cases}$$$

Lean4

@[grind =]
theorem hyperoperation_ge_four_zero (n k : ℕ) : hyperoperation (n + 4) 0 k = if Even k then 1 else 0 := by
  induction k with grind

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