Naturals pairing function #
This file defines a pairing function for the naturals as follows:
0 1 4 9 16
2 3 5 10 17
6 7 8 11 18
12 13 14 15 19
20 21 22 23 24
It has the advantage of being monotone in both directions and sending ⟦0, n^2 - 1⟧
to
⟦0, n - 1⟧²
.
@[simp]
An equivalence between ℕ × ℕ
and ℕ
.
Equations
- Nat.pairEquiv = { toFun := Function.uncurry Nat.pair, invFun := Nat.unpair, left_inv := Nat.pairEquiv.proof_1, right_inv := Nat.pair_unpair }
theorem
supᵢ_unpair
{α : Type u_1}
[inst : CompleteLattice α]
(f : ℕ → ℕ → α)
:
(⨆ n, f (Nat.unpair n).fst (Nat.unpair n).snd) = ⨆ i, ⨆ j, f i j
theorem
infᵢ_unpair
{α : Type u_1}
[inst : CompleteLattice α]
(f : ℕ → ℕ → α)
:
(⨅ n, f (Nat.unpair n).fst (Nat.unpair n).snd) = ⨅ i, ⨅ j, f i j
theorem
Set.unionᵢ_unpair_prod
{α : Type u_1}
{β : Type u_2}
{s : ℕ → Set α}
{t : ℕ → Set β}
:
(Set.unionᵢ fun n => s (Nat.unpair n).fst ×ˢ t (Nat.unpair n).snd) = (Set.unionᵢ fun n => s n) ×ˢ Set.unionᵢ fun n => t n
theorem
Set.unionᵢ_unpair
{α : Type u_1}
(f : ℕ → ℕ → Set α)
:
(Set.unionᵢ fun n => f (Nat.unpair n).fst (Nat.unpair n).snd) = Set.unionᵢ fun i => Set.unionᵢ fun j => f i j
theorem
Set.interᵢ_unpair
{α : Type u_1}
(f : ℕ → ℕ → Set α)
:
(Set.interᵢ fun n => f (Nat.unpair n).fst (Nat.unpair n).snd) = Set.interᵢ fun i => Set.interᵢ fun j => f i j