ack_mono_left

Mathlib.Computability.Ackermann

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

← MathLib Explorer

English

For every n, the function m ↦ ack(m, n) is monotone nondecreasing in m.

Русский

Для каждого n функция m ↦ ack(m, n) неубывает по m.

LaTeX

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

Lean4

theorem ack_mono_left (n : ℕ) : Monotone fun m => ack m n :=
  (ack_strictMono_left n).monotone

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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