From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 10 Feb 2024 02:22:14 +0100
Subject: Initial commit

---
 library/set/cantor.tex | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 library/set/cantor.tex

(limited to 'library/set/cantor.tex')

diff --git a/library/set/cantor.tex b/library/set/cantor.tex
new file mode 100644
index 0000000..f7c4b2b
--- /dev/null
+++ b/library/set/cantor.tex
@@ -0,0 +1,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}
-- 
cgit v1.2.3