max_ack_left — Mathlib

English

The Ackermann function commutes with taking maximum: ack(max(m1,m2), n) = max(ack(m1,n), ack(m2,n)).

Русский

Функция Аккермана коммутирует с максимумом: ack(max(m1,m2), n) = max(ack(m1,n), ack(m2,n)).

LaTeX

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

Lean4

theorem max_ack_left (m₁ m₂ n : ℕ) : ack (max m₁ m₂) n = max (ack m₁ n) (ack m₂ n) :=
  (ack_mono_left n).map_max

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