ack_injective_left

Mathlib.Computability.Ackermann

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

English

For fixed n, the map m ↦ ack(m, n) is injective.

Русский

Для фиксированного n отображение m ↦ ack(m, n) инъективно.

LaTeX

$$$$\\forall n \\in \\mathbb{N},\\ ∀ m_1,m_2 \\in \\mathbb{N},\\ \operatorname{ack}(m_1,n) = \\operatorname{ack}(m_2,n) \\Rightarrow m_1 = m_2.$$$$

Lean4

theorem ack_injective_left (n : ℕ) : Function.Injective fun m => ack m n :=
  (ack_strictMono_left n).injective

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

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

Разделы

Аффилиация

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