ack_pair_lt

Mathlib.Computability.Ackermann

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

← MathLib Explorer

English

For all m,n,k, ack(m, pair(n,k)) < ack(m+4, max(n,k)).

Русский

Для всех m,n,k: ack(m, пары(n,k)) < ack(m+4, max(n,k)).

LaTeX

$$$$\\forall m,n,k \\in \\mathbb{N}, \\operatorname{ack}(m, \\operatorname{pair}(n,k)) < \\operatorname{ack}(m+4, \\max(n,k)).$$$$

Lean4

theorem ack_pair_lt (m n k : ℕ) : ack m (pair n k) < ack (m + 4) (max n k) :=
  (ack_strictMono_right m <| pair_lt_max_add_one_sq n k).trans <| ack_add_one_sq_lt_ack_add_four _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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