add_lt_ack — Mathlib

English

For all m,n, m+n < ack m n.

Русский

Для всех m,n: m+n < A(m,n).

LaTeX

$$$$\forall m,n \in \mathbb{N},\ m+n < \operatorname{ack}(m,n).$$$$

Lean4

theorem add_lt_ack : ∀ m n, m + n < ack m n
  | 0, n => by simp
  | m + 1, 0 => by simpa using add_lt_ack m 1
  | m + 1, n + 1 =>
    calc
      m + 1 + n + 1 ≤ m + (m + n + 2) := by omega
      _ < ack m (m + n + 2) := (add_lt_ack _ _)
      _ ≤ ack m (ack (m + 1) n) :=
        (ack_mono_right m <| le_of_eq_of_le (by rw [succ_eq_add_one]; ring_nf) <| succ_le_of_lt <| add_lt_ack (m + 1) n)
      _ = ack (m + 1) (n + 1) := (ack_succ_succ m n).symm

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