pairEquiv — Mathlib

English

There is a bijection between pairs of naturals and naturals, given by the pairing and unpairing operations.

Русский

Существует биекция между парами натуральных чисел и натуральными числами, заданная операциями кодирования и распаковки.

LaTeX

$$$ \operatorname{pairEquiv} : (\mathbb{N} \times \mathbb{N}) \simeq \mathbb{N}. $$$

Lean4

/-- An equivalence between `ℕ × ℕ` and `ℕ`. -/
@[simps -fullyApplied]
def pairEquiv : ℕ × ℕ ≃ ℕ :=
  ⟨uncurry pair, unpair, fun ⟨a, b⟩ => unpair_pair a b, pair_unpair⟩

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