blob: 700295bca9cc83eb70fc791075002f3c547636ea (
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
|
\import{set/powerset.tex}
\import{function.tex}
\subsection{Fixpoints}
% NOTE: we need to explicitly require that a is an element of the domain,
% otherwise the emptyset becomes a fixpoint when it's not in the domain.
\begin{definition}\label{fixpoint}
$a$ is a fixpoint of $f$ iff $a\in\dom{f}$ and $f(a) = a$.
\end{definition}
\begin{definition}\label{subseteqpreserving}
$f$ is \subseteq-preserving iff
for all $A, B\in\dom{f}$ such that $A\subseteq B$ we have $f(A)\subseteq f(B)$.
\end{definition}
\begin{theorem}[Knaster--Tarski]\label{knastertarski}
Let $f$ be a \subseteq-preserving function from $\pow{A}$ to $\pow{A}$.
Then there exists a fixpoint of $f$.
\end{theorem}
\begin{proof}
$\dom{f} = \pow{A}$.
Let $P = \{a\in\pow{A}\mid a\subseteq f(a)\}$.
$P\subseteq\pow{A}$.
Thus $\unions{P}\in\pow{A}$.
Hence $f(\unions{P})\in\pow{A}$ by \cref{funs_type_apply}.
Show $\unions{P}\subseteq f(\unions{P})$.
\begin{subproof}
It suffices to show that every element of $\unions{P}$ is an element of $f(\unions{P})$.
%
Fix $u\in\unions{P}$.
%
Take $p\in P$ such that $u\in p$.
Then $u\in f(p)$.
$p\subseteq\unions{P}$.
$f(p)\subseteq f(\unions{P})$ by \cref{subseteqpreserving}.
Thus $u\in f(\unions{P})$.
\end{subproof}
Now $f(\unions{P})\subseteq f(f(\unions{P}))$ by \cref{subseteqpreserving}.
Thus $f(\unions{P})\in P$ by definition.
Hence $f(\unions{P})\subseteq \unions{P}$.
Thus $f(\unions{P}) = \unions{P}$ by \cref{subseteq_antisymmetric}.
Follows by \cref{fixpoint}.
\end{proof}
|
