Skip to content
Journals Garden

Diagonal Sweeping Order (対角掃引順序) (Example I.3.4)

  • Diagonal Sweeping Order (対角掃引順序) (Example I.3.4) #Card
    • The linear order on $\mathbb{N} \times \mathbb{N}$: $(n_0, k_0) \prec (n_1, k_1) \iff n_0 + k_0 < n_1 + k_1$, or $n_0 + k_0 = n_1 + k_1$ and $n_0 < n_1$.

Back

Section titled “Back”

On $\mathbb{N} \times \mathbb{N}$ define $$(n_0, k_0) \prec (n_1, k_1) \iff (n_0 + k_0 < n_1 + k_1) \vee (n_0 + k_0 = n_1 + k_1 \wedge n_0 < n_1),$$ and $(n_0,k_0) \preccurlyeq (n_1,k_1)$ by $\prec$ or equality. This is a linear order: all elements of $\mathbb{N} \times \mathbb{N}$ can be arranged in a sequence $$(0,0), (0,1), (1,0), (0,2), (1,1), (2,0), (0,3), (1,2), \dots$$ （無限行列を反対角線に沿って掃く）。

  • $\mathbb{N} \times \mathbb{N}$ が可算であることの構成的証明であり、可算和の可算性（cards/topology/prop-i-5-4）・$\mathbb{Q}$ の可算性の土台。

Lean

Section titled “Lean”

Nat.pairEquiv / Denumerable (ℕ × ℕ)（Cantor pairing）