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⟧²
.
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 }
Instances For
theorem
iSup_unpair
{α : Type u_1}
[CompleteLattice α]
(f : ℕ → ℕ → α)
:
⨆ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⨆ i, ⨆ j, f i j
theorem
iInf_unpair
{α : Type u_1}
[CompleteLattice α]
(f : ℕ → ℕ → α)
:
⨅ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⨅ i, ⨅ j, f i j
theorem
Set.iUnion_unpair_prod
{α : Type u_1}
{β : Type u_2}
{s : ℕ → Set α}
{t : ℕ → Set β}
:
⋃ n, s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2 = (⋃ n, s n) ×ˢ ⋃ n, t n
theorem
Set.iUnion_unpair
{α : Type u_1}
(f : ℕ → ℕ → Set α)
:
⋃ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⋃ i, ⋃ j, f i j
theorem
Set.iInter_unpair
{α : Type u_1}
(f : ℕ → ℕ → Set α)
:
⋂ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⋂ i, ⋂ j, f i j