summaryrefslogtreecommitdiff
path: root/library/set/cantor.tex
blob: f7c4b2b1b9578a58e7f75dfadb10c2308d75c1d2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
\import{set/powerset.tex}
\import{function.tex}

\subsection{Cantor's theorem}


\begin{theorem}[Cantor]\label{cantor}
    There exists no surjection from $A$ to $\pow{A}$.
\end{theorem}
\begin{proof}
    Suppose not.
    Consider a surjection $f$ from $A$ to $\pow{A}$.
    Let $B = \{a \in A \mid a\notin f(a)\}$.
    Then $B\in\pow{A}$.
    There exists $a'\in A$ such that $f(a') = B$ by \hyperref[surj]{the definition of surjectivity}.
    Now $a' \in B$ iff $a' \notin f(a') = B$.
    Contradiction.
\end{proof}