▾ 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
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}
Child definitions
» D1880: Cofinite set
Results
» R1744: Finite union of finite sets is finite
» R1743: Intersection of finite sets is finite
» R477: Set finiteness is hereditary
» R4292: Finite cartesian product of finite sets is finite
» R4293: Power set of a finite set is finite
» R4294: Set difference with finite minuend is finite