\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}$ by \cref{funs_elim}.
    Let $P = \{a\in\pow{A}\mid a\subseteq f(a)\}$.
    $P\subseteq\pow{A}$ by \cref{subseteq}.
    Thus $\unions{P}\in\pow{A}$ by \cref{powerset_closed_unions}.
    Hence $f(\unions{P})\in\pow{A}$ by \cref{funs_type_apply}.

    Show for all $u$ we have if $u\in\unions{P}$, then $u\in f(\unions{P})$.
    \begin{subproof}
        Fix $u$.
        Assume $u\in\unions{P}$.
        Take $p$ such that $p\in P$ and $u\in p$ by \cref{unions_iff}.
        We have $p\subseteq f(p)$ by assumption.
        Thus $u\in f(p)$ by \cref{subseteq}.
        We have $p\subseteq\unions{P}$ by \cref{subseteq,unions_iff}.
        We have $f(p)\subseteq f(\unions{P})$ by \cref{subseteqpreserving}.
        Follows by \cref{subseteq}.
    \end{subproof}
    Thus $\unions{P}\subseteq f(\unions{P})$ by \cref{subseteq}.

    Now $f(\unions{P})\subseteq f(f(\unions{P}))$ by \cref{subseteqpreserving}.
    Thus $f(\unions{P})\in P$ by assumption.

    Hence $f(\unions{P})\subseteq \unions{P}$ by \cref{subseteq,unions_iff}.

    Thus $f(\unions{P}) = \unions{P}$ by \cref{subseteq_antisymmetric}.
    Follows by \cref{fixpoint}.
\end{proof}