ack_inj_left

Mathlib.Computability.Ackermann

URI: https://scilib.ai/kg/mathlib#ack_inj_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) = ack(m_2,n) \\iff m_1 = m_2.$$$$

Lean4

@[simp]
theorem ack_inj_left {m₁ m₂ n : ℕ} : ack m₁ n = ack m₂ n ↔ m₁ = m₂ :=
  (ack_injective_left n).eq_iff

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

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

Разделы

Аффилиация

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