ack_inj_right

Mathlib.Computability.Ackermann

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

English

For all m, n1, n2, ack m n1 = ack m n2 iff n1 = n2.

Русский

Для всех m, n1, n2: A(m,n1) = A(m,n2) тогда и только тогда, когда n1 = n2.

LaTeX

$$$$\forall m,n_1,n_2 \in \mathbb{N},\ \operatorname{ack}(m,n_1) = \operatorname{ack}(m,n_2) \iff n_1 = n_2.$$$$

Lean4

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

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

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

Разделы

Аффилиация

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