Let $\mathbb{N}$ be the D225: Set of natural numbers.
A D11: Set $X$ is a finite set if and only if
\begin{equation}
\exists \, N \in \mathbb{N} :
\text{Bij}(\{ 1, \ldots, N \} \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 |
▼ | Countable set |
▶ | D1880: Cofinite set |
▶ | R4292: Finite cartesian product of finite sets is finite |