lt_ack_right

Mathlib.Computability.Ackermann

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

English

For all natural numbers m and n, n is strictly less than the Ackermann function at (m, n).

Русский

Для всех натуральных чисел m и n выполняется n < Ackermann(m, n).

LaTeX

$$$$\\forall m,n \\in \\mathbb{N},\\ n < \\operatorname{ack}(m,n).$$$$

Lean4

theorem lt_ack_right (m n : ℕ) : n < ack m n :=
  (self_le_add_left n m).trans_lt <| add_lt_ack m n

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

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

Разделы

Аффилиация

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