ack_lt_iff_right

Mathlib.Computability.Ackermann

URI: https://scilib.ai/kg/mathlib#ack_lt_iff_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_lt_iff_right {m n₁ n₂ : ℕ} : ack m n₁ < ack m n₂ ↔ n₁ < n₂ :=
  (ack_strictMono_right m).lt_iff_lt

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

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

Разделы

Аффилиация

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