max_ack_right — Mathlib

English

Ackermann is monotone with respect to the second argument: A(m, max(n1,n2)) = max(A(m,n1), A(m,n2)).

Русский

Функция Аккермана монотонна по второму аргументу: A(m, max(n1,n2)) = max(A(m,n1), A(m,n2)).

LaTeX

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

Lean4

theorem max_ack_right (m n₁ n₂ : ℕ) : ack m (max n₁ n₂) = max (ack m n₁) (ack m n₂) :=
  (ack_mono_right m).map_max

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