ack_le_iff_left

Mathlib.Computability.Ackermann

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

English

For all m1, m2, n, 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) \\le \\operatorname{ack}(m_2,n) \\iff m_1 \\le m_2.$$$$

Lean4

@[simp]
theorem ack_le_iff_left {m₁ m₂ n : ℕ} : ack m₁ n ≤ ack m₂ n ↔ m₁ ≤ m₂ :=
  (ack_strictMono_left n).le_iff_le

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

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

Разделы

Аффилиация

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