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

Let $\mathbb{N}$ be the D225: Set of natural numbers.
A D11: Set $X$ is a countable set if and only if $$\exists \, E \subseteq \mathbb{N} : \text{Bij}(E \to X) \neq \emptyset$$

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
 ▶ D1881: Cocountable set ▶ D17: Finite set
Results
 ▶ R4627 ▶ R263: Binary cartesian product of countable sets is countable ▶ R3507: Binary union of countable sets is countable ▶ R371: Countable set iff injection to natural numbers ▶ R262: Countable union of countable sets is countable ▶ R508: Finite cartesian product of countable sets is countable ▶ R3506: Finite union of countable sets is countable ▶ R511: Natural number plane is countable