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
Formulation 0
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}
Formulation 1
Let $\mathbb{N}$ be the D225: Set of natural numbers.
A D11: Set $X$ is a countable set if and only if there exists a D18: Map $f : E \to X$ such that
(1) $E \subseteq \mathbb{N}$ is a D78: Subset of $\mathbb{N}$
(2) $f$ is a D468: Bijective map from $E$ to $X$
Child definitions
» D1881: Cocountable set
» D17: Finite set
Results
» R262: Countable union of countable sets is countable
» R263: Binary cartesian product of countable sets is countable
» R431: Set of integers is countable
» R432: Set of natural numbers is countable
» R368: Image of countable set is countable
» R507: Empty set is countable
» R508: Finite cartesian product of countable sets is countable
» R371: Countable set iff injection to natural numbers
» R3506: Finite union of countable sets is countable
» R3507: Binary union of countable sets is countable
» R4627:
» R370: Countable set iff surjection from natural numbers
» R4295: Power set of a countable set need not be countable
» R511: Natural number plane is countable
» R104: Set of rational numbers is countable