library/cardinal.tex


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

\section{Cardinality}\label{form_sec_cardinality}

\import{set.tex}
\import{ordinal.tex}
\import{function.tex}
\import{numbers.tex}

\begin{definition}\label{finite}
    $X$ is finite iff there exists a natural number $k$ such that
        there exists a bijection from $k$ to $X$.
\end{definition}

\begin{abbreviation}\label{infinite}
    $X$ is infinite iff $X$ is not finite.
\end{abbreviation}

\begin{definition}\label{cardinality}
    $X$ has cardinality $k$ iff $k$ is a natural number and 
    there exists a bijection from $k$ to $X$.
\end{definition}