ack_add_one_sq_lt_ack_add_three — Mathlib

English

For all m,n, (ack(m,n) + 1)^2 ≤ ack(m+3, n).

Русский

Для всех m,n: (ack(m,n) + 1)^2 ≤ ack(m+3, n).

LaTeX

$$$$\\forall m,n \\in \\mathbb{N}, \\bigl(\\operatorname{ack}(m,n) + 1\\bigr)^2 \\le \\operatorname{ack}(m+3, n).$$$$

Lean4

theorem ack_add_one_sq_lt_ack_add_three : ∀ m n, (ack m n + 1) ^ 2 ≤ ack (m + 3) n
  | 0, n => by simpa using sq_le_two_pow_add_one_minus_three (n + 2)
  | m + 1, 0 => by
    rw [ack_succ_zero, ack_succ_zero]
    apply ack_add_one_sq_lt_ack_add_three
  | m + 1, n + 1 => by
    rw [ack_succ_succ, ack_succ_succ]
    apply (ack_add_one_sq_lt_ack_add_three _ _).trans (ack_mono_right _ <| ack_mono_left _ _)
    cutsat

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