ack_strictMono_right — Mathlib

English

For each m, the function n ↦ ack m n is strictly increasing.

Русский

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

LaTeX

$$$$\forall m\in\mathbb{N},\ \text{StrictMono}(n \mapsto \operatorname{ack}(m,n)).$$$$

Lean4

theorem ack_strictMono_right : ∀ m, StrictMono (ack m)
  | 0, n₁, n₂, h => by simpa using h
  | m + 1, 0, n + 1, _h => by
    rw [ack_succ_zero, ack_succ_succ]
    exact ack_strictMono_right _ (one_lt_ack_succ_left m n)
  | m + 1, n₁ + 1, n₂ + 1, h => by
    rw [ack_succ_succ, ack_succ_succ]
    apply ack_strictMono_right _ (ack_strictMono_right _ _)
    rwa [add_lt_add_iff_right] at h

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