pair_lt_max_add_one_sq — Mathlib

English

Pairing is strictly below the square of max(m,n) plus one: pair(m,n) < (max(m,n) + 1)^2.

Русский

Кодирование пары всегда строго меньше квадрата max(m,n) плюс единица: pair(m,n) < (max(m,n) + 1)^2.

LaTeX

$$$ \forall m,n \in \mathbb{N}, \; \operatorname{pair}(m,n) < (\max(m,n) + 1)^2. $$$

Lean4

theorem pair_lt_max_add_one_sq (m n : ℕ) : pair m n < (max m n + 1) ^ 2 :=
  by
  simp only [pair, Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul, Nat.add_assoc]
  split_ifs <;> simp [Nat.le_of_lt, not_lt.1, *] <;> omega

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