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
Definition D16
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$
Children
Cocountable set
Finite set
Results
R4627
Binary cartesian product of countable sets is countable
Binary union of countable sets is countable
Countable set iff injection to natural numbers
Countable union of countable sets is countable
Finite cartesian product of countable sets is countable
Finite union of countable sets is countable
Natural number plane is countable