summaryrefslogtreecommitdiff
path: root/library/cardinal.tex
diff options
context:
space:
mode:
Diffstat (limited to 'library/cardinal.tex')
-rw-r--r--library/cardinal.tex10
1 files changed, 9 insertions, 1 deletions
diff --git a/library/cardinal.tex b/library/cardinal.tex
index d0dec59..5682619 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -1,8 +1,9 @@
-\section{Cardinality}
+\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
@@ -12,3 +13,10 @@
\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}
+
+