ack_le_ack — Mathlib

English

If m1 ≤ m2 and n1 ≤ n2 then ack m1 n1 ≤ ack m2 n2.

Русский

Если m1 ≤ m2 и n1 ≤ n2, то ack(m1,n1) ≤ ack(m2,n2).

LaTeX

$$$$\\forall {m_1,m_2,n_1,n_2} \\in \\mathbb{N}, \\ m_1 \\le m_2 \\land \\ n_1 \\le n_2 \\Rightarrow \\ ack(m_1,n_1) \\le \\ ack(m_2,n_2).$$$$

Lean4

@[gcongr]
theorem ack_le_ack {m₁ m₂ n₁ n₂ : ℕ} (hm : m₁ ≤ m₂) (hn : n₁ ≤ n₂) : ack m₁ n₁ ≤ ack m₂ n₂ :=
  (ack_mono_left n₁ hm).trans <| ack_mono_right m₂ hn

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