ack_lt_iff_left

Mathlib.Computability.Ackermann

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

English

For all m1, m2, n, the strict inequality holds: ack(m1, n) < ack(m2, n) iff m1 < m2.

Русский

Для всех m1, m2, n верно: ack(m1, n) < ack(m2, n) при неравенстве m1 < m2, и наоборот.

LaTeX

$$$$\\forall {m_1,m_2,n} \\in \\mathbb{N},\\ ack(m_1,n) < ack(m_2,n) \\iff m_1 < m_2.$$$$

Lean4

@[simp]
theorem ack_lt_iff_left {m₁ m₂ n : ℕ} : ack m₁ n < ack m₂ n ↔ m₁ < m₂ :=
  (ack_strictMono_left n).lt_iff_lt

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

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

Разделы

Аффилиация

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