\documentclass[../../set-theory/set-theory.tex]{subfiles}

\begin{document}
  \chapter{Fixed points}\label{chapter:fixed-points}

  \filename{foundations/sections/12_fixed-points.ftl.tex}

  \begin{forthel}
    %[prove off][check off]

    [readtex \path{foundations/sections/10_sets.ftl.tex}]

    %[prove on][check on]
  \end{forthel}


  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_12_2177076576649216}
      Let $f$ be a map.
      A fixed point of $f$ is an element $x$ of $\dom(f)$ such that $f(x) = x$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_12_1394550966845440}
      A map between systems of sets is a map from some system of sets to some
      system of sets.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_12_3290499861446656}
      Let $f$ be a map between systems of sets.
      $f$ is subset preserving iff for all $x, y \in \dom(f)$
      \[ x \subseteq y \implies f(x) \subseteq f(y). \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}[Knaster-Tarski]\printlabel{FOUNDATIONS_12_8420450166112256}
      Let $x$ be a set.
      Let $f$ be a subset preserving map from $\pow(x)$ to $\pow(x)$.
      Then $f$ has a fixed point.
    \end{theorem}
    \begin{proof}
      (1) Define $A = \{ y \mid y \subseteq x$ and $y \subseteq f(y) \}$.
      Then $A$ is a subset of $\pow(x)$.
      We have $\bigcup A \in \pow(x)$.

      Let us show that (2) $\bigcup A \subseteq f(\bigcup A)$.
        Let $u \in \bigcup A$.
        Take $y \in A$ such that $u \in y$.
        Then $u \in f(y)$.
        We have $y \subseteq \bigcup A$.
        Hence $f(y) \subseteq f(\bigcup A)$.
        Thus $f(y) \subseteq f(\bigcup A)$.
        Therefore $u \in f(\bigcup A)$.
      End.

      Then $f(\bigcup A) \in A$ (by 1).
      Indeed $f(\bigcup A) \subseteq x$.
      (3) Hence $f(\bigcup A) \subseteq \bigcup A$.
      Indeed every element of $f(\bigcup A)$ is an element of some element of
      $A$.

      Thus $f(\bigcup A) = \bigcup A$ (by 2, 3).
    \end{proof}
  \end{forthel}
\end{document}
