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

▾ Alphabet

▾ Deduction system

▾ Theory

▾ Zermelo-Fraenkel set theory

▾ Set

▾ Binary cartesian set product

▾ Binary relation

▾ Map

▾ Bijective map

▾ Set of bijections

▾ Countable set

Formulation 0

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}

A D11: Set $X$ is a

Child definitions

Results