blob: a846b7814999cd376265861ce4aff1fe4fcf0a86 (
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
|
\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_is_bijection}.
Follows by \cref{equinum}.
\end{proof}
\begin{proposition}\label{equinum_sym}
Suppose $A\approx B$. Then $B\approx A$.
\end{proposition}
\begin{proof}
Take a bijection $f$ 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 a bijection $f$ from $A$ to $B$ by \cref{equinum}.
Take a bijection $g$ 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}
Let $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ for $X\in\pow{A}$.
%By construction: $h$ is a relation.
%By construction: $h$ is right-unique.
%By construction: $\dom{h} = \pow{A}$.
For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by \cref{setminus_subseteq,pow_iff}.
Thus $h$ is a function from $\pow{A}$ to $\pow{A}$.
$h$ is \subseteq-preserving by \cref{subseteqpreserving,img_subseteq,subseteq_implies_setminus_supseteq}. % apply each each lemma twice (alternating).
Take a fixpoint $X$ 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}
|
