ThmDex – An index of mathematical definitions, results, and conjectures.
▼ 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
Definition D17
Finite 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}
Children
▶ D1880: Cofinite set
Results
▶ R4292: Finite cartesian product of finite sets is finite