hyperoperation_ge_three_one

Mathlib.Data.Nat.Hyperoperation

URI: https://scilib.ai/kg/mathlib#hyperoperation_ge_three_one

English

For all n,k ∈ ℕ, H_{n+3}(1,k) = 1.

Русский

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

LaTeX

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

Lean4

@[grind =]
theorem hyperoperation_ge_three_one (n k : ℕ) : hyperoperation (n + 3) 1 k = 1 := by
  induction n generalizing k with grind [cases Nat]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru