one_lt_ack_succ_right

Mathlib.Computability.Ackermann

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

English

For all m,n, 1 < ack m (n+1).

Русский

Для всех m,n: 1 < ack(m,n+1).

LaTeX

$$$$1 < \operatorname{ack}(m,n+1).$$$$

Lean4

theorem one_lt_ack_succ_right : ∀ m n, 1 < ack m (n + 1)
  | 0, n => by simp
  | m + 1, n => one_lt_ack_succ_left m (n + 1)

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

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

Разделы

Аффилиация

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