blob: 7c12d7ab12637c920ab872e17bf8212331e5a01d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
\import{set/powerset.tex}
\import{set/fixpoint.tex}
\import{function.tex}
\begin{definition}\label{equinum}
$A$ is equinumerous with $B$ iff there exists a bijection from $A$ to $B$.
\end{definition}
\begin{abbreviation}\label{approx}
$A\approx B$ iff $A$ is equinumerous with $B$.
\end{abbreviation}
\begin{proposition}\label{equinum_refl}
$A\approx A$.
\end{proposition}
\begin{proof}
$\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_elem_bijections}.
Follows by \cref{equinum}.
\end{proof}
\begin{proposition}\label{equinum_sym}
Suppose $A\approx B$. Then $B\approx A$.
\end{proposition}
\begin{proof}
Take $f$ such that $f$ is a bijection from $A$ to $B$ by \cref{equinum}.
Then $\converse{f}$ is a bijection from $B$ to $A$ by \cref{bijection_converse_is_bijection}.
Follows by \cref{equinum}.
\end{proof}
\begin{proposition}\label{equinum_tran}
Suppose $A\approx B\approx C$. Then $A\approx C$.
\end{proposition}
\begin{proof}
Take $f$ such that $f$ is a bijection from $A$ to $B$ by \cref{equinum}.
Take $g$ such that $g$ is a bijection from $B$ to $C$ by \cref{equinum}.
Then $g\circ f$ is a bijection from $A$ to $C$ by \cref{bijection_circ}.
Follows by \cref{equinum}.
\end{proof}
\begin{theorem}[Cantor--Schröder--Bernstein]\label{cantorschroederbernstein}
Let $f$ be an injective function from $A$ to $B$.
Let $g$ be an injective function from $B$ to $A$.
Then $A\approx B$.
\end{theorem}
\begin{proof}
For all $X\in\pow{A}$ we have
$A\setminus \img{g}{B\setminus\img{f}{X}}\subseteq A$
by \cref{setminus_subseteq}.
For all $X\in\pow{A}$ we have
$A\setminus \img{g}{B\setminus\img{f}{X}}\in\pow{A}$
by \cref{powerset_intro}.
Let $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ for $X\in\pow{A}$.
For all $X\in\pow{A}$ we have
$(X,A\setminus \img{g}{B\setminus\img{f}{X}})\in h$ by assumption.
$h$ is a relation by \cref{relation}.
$h$ is right-unique by \cref{rightunique,pair_eq_iff}.
Thus $h$ is a function by assumption.
For all $X\in\pow{A}$ we have
$h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$
by \cref{function_apply_intro}.
For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by assumption.
For all $X$ we have if $X\in\dom{h}$, then $X\in\pow{A}$
by \cref{dom_iff,pair_eq_iff}.
For all $X$ we have if $X\in\pow{A}$, then $X\in\dom{h}$
by \cref{dom_iff}.
Thus $\dom{h} = \pow{A}$ by set extensionality.
$h$ is a function to $\pow{A}$ by assumption.
Thus $h$ is a function from $\pow{A}$ to $\pow{A}$ by \cref{funs_intro}.
$h$ is \subseteq-preserving by \cref{subseteqpreserving,img_subseteq,subseteq_implies_setminus_supseteq}. % apply each each lemma twice (alternating).
Take $X$ such that $X$ is a fixpoint of $h$ by \cref{knastertarski}.
Now $X = A\setminus \img{g}{B\setminus\img{f}{X}}$ by \cref{fixpoint}.
$\img{g}{B\setminus\img{f}{X}}\subseteq A$.
Thus $\img{g}{B\setminus\img{f}{X}} = A\setminus X$ by \cref{double_relative_complement}.
Let $h' = \restrl{h}{X}$.
Omitted. % TODO
\end{proof}
|
