Let $\mathbb{N}$ be the D225: Set of natural numbers.
A D11: Set $X$ is a countable set if and only if
\begin{equation}
\exists \, E \subseteq \mathbb{N} :
\text{Bij}(E \to X)
\neq \emptyset
\end{equation}
| ▼ | Set of symbols |
| ▼ | Alphabet |
| ▼ | Deduction system |
| ▼ | Theory |
| ▼ | Zermelo-Fraenkel set theory |
| ▼ | Set |
| ▼ | Binary cartesian set product |
| ▼ | Binary relation |
| ▼ | Map |
| ▼ | Bijective map |
| ▼ | Set of bijections |
| (1) | $E \subseteq \mathbb{N}$ is a D78: Subset of $\mathbb{N}$ |
| (2) | $f$ is a D468: Bijective map from $E$ to $X$ |
| ▶ | D1881: Cocountable set |
| ▶ | D17: Finite set |