hyperoperation_recursion — Mathlib

English

For all n,m,k in N, hyperoperation(n+1) m (k+1) = hyperoperation n m (hyperoperation(n+1) m k).

Русский

Для всех n,m,k натуральных: hyperoperation(n+1) m (k+1) = hyperoperation n m (hyperoperation(n+1) m k).

LaTeX

$$$\forall n,m,k \in \mathbb{N}, \ hyperoperation(n+1,m,k+1) = \ hyperoperation(n,m,\ hyperoperation(n+1,m,k))$$$

Lean4

@[grind =]
theorem hyperoperation_recursion (n m k : ℕ) :
    hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k) := by
  grind
    -- Interesting hyperoperation lemmas

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