\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{mathtools}
\usepackage{xr}
\usepackage[foundations, settheory]{../lib/tex/naproche}

\externaldocument{set-theory/set-theory}

\title{König's Theorem}
\author{\Naproche formalization: \vspace{0.5em} \\
Steffen Frerix and Peter Koepke \\
University of Bonn}
\date{2018 - 2021}

\newcommand{\SumSet}[2]{\bigsqcup_{i \in #2} #1_{i}}
\newcommand{\Sum}[2]{\sum_{i \in #2} #1_{i}}
\newcommand{\ProdSet}[2]{\bigtimes_{i \in #2} #1_{i}}
\newcommand{\Prod}[2]{\prod_{i \in #2} #1_{i}}


\begin{document}

\maketitle

\noindent König's Theorem is an important set-theoretical result about the
arithmetic of cardinals.
It was proved by Julius König in 1905 \cite[p. 177--180]{Koenig1905}.
The proof is reminiscent of Cantor's diagonal argument for proving that
$\kappa < 2^\kappa$.

On mid-range hardware \Naproche needs approximately 2 Minutes to verify this
formalization plus approximately 25 minutes to verify the library files it
depends on.

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

  [readtex \path{set-theory/sections/06_cardinals.ftl.tex}]

  %[prove on][check on]

  Let $f_{i}$ stand for $f(i)$.
\end{forthel}


\section*{Sums and Products of cardinals}

\begin{forthel}
  Let $D$ denote a set.

  \begin{definition*}
    A sequence of cardinals on $D$ is a function $\kappa$ such that
    $\dom(\kappa) = D$ and $\kappa_{i}$ is a cardinal for every element $i$ of
    $D$.
  \end{definition*}

  \begin{definition*}
    Let $\kappa$ be a sequence of cardinals on $D$.
    \[ \SumSet{\kappa}{D} = \class{(n,i) | \text{$i$ is an element of $D$ and
    $n$ is an element of $\kappa_{i}$}}. \]
  \end{definition*}

  \begin{axiom*}
    Let $\kappa$ be a sequence of cardinals on $D$.
    Then $\SumSet{\kappa}{D}$ is a set.
  \end{axiom*}

  \begin{definition*}
    Let $\kappa$ be a sequence of cardinals on $D$.
    \[ \Sum{\kappa}{D} = \left| \SumSet{\kappa}{D} \right|. \]
  \end{definition*}

  \begin{definition*}
    Let $\kappa$ be a sequence of cardinals on $D$.
    \[ \ProdSet{\kappa}{D} = \class{f | \classtext{$f$ is a function and
    $\dom(f) = D$ and $f(i)$ is an element of $\kappa_{i}$ for every element
    $i$ of $D$}}. \]
  \end{definition*}

  \begin{axiom*}
    Let $\kappa$ be a sequence of cardinals on $D$.
    Then $\ProdSet{\kappa}{D}$ is a set.
  \end{axiom*}

  \begin{definition*}
    Let $\kappa$ be a sequence of cardinals on $D$.
    \[ \Prod{\kappa}{D} = \left| \ProdSet{\kappa}{D} \right|. \]
  \end{definition*}
\end{forthel}

König's Theorem requires some form of the axiom of choice.
Currently choice is built into Naproche by the \emph{choose} construct in
function definitions.
The axiom of choice is also required to show that products of non-empty factors
are themselves non-empty:

\begin{forthel}
  \begin{lemma*}[Choice]
    Let $\lambda$ be a sequence of cardinals on $D$.
    Assume that $\lambda_{i}$ has an element for every element $i$ of $D$.
    Then $\ProdSet{\lambda}{D}$ has an element.
  \end{lemma*}
  \begin{proof}
    Define $f(i) =$ ``choose an element $v$ of $\lambda_{i}$ in $v$'' for $i$
    in $D$.
    Then $f$ is an element of $\ProdSet{\lambda}{D}$.
  \end{proof}
\end{forthel}


\section*{König's theorem}

\begin{forthel}
  \begin{theorem*}[König]\label{koenig}
    Let $\kappa, \lambda$ be sequences of cardinals on $D$.
    Assume that for every element $i$ of $D$ $\kappa_{i} < \lambda_{i}$.
    Then \[ \Sum{\kappa}{D} < \Prod{\lambda}{D}. \]
  \end{theorem*}
  \begin{proof}[by contradiction]
    Assume the contrary.
    Then \[ \Prod{\lambda}{D} \leq \Sum{\kappa}{D}. \]
    Take a surjective map $G$ from $\SumSet{\kappa}{D}$ to
    $\ProdSet{\lambda}{D}$.
    Indeed $\ProdSet{\lambda}{D}$ and $\Sum{\kappa}{D}$ are nonempty sets.
    Take $\Lambda = \bigcup \range(\lambda)$.
    Then $\Lambda$ is a set.
    Indeed $\range(\lambda)$ is a set.

    Define $\Delta(i) = \{ G(n,i)(i) \in \Lambda \mid n \in \kappa_{i} \}$ for
    $i \in D$.

    For every element $f$ of $\ProdSet{\lambda}{D}$ and every element $i$ of $D$
    we have $f(i) \in \Lambda$.

    For every element $i$ of $D$ we have $|\Delta(i)| < \lambda_{i}$. \\
    Proof.
      Let $i$ be an element of $D$.
      Define $F(n) = G(n,i)(i)$ for $n$ in $\kappa_{i}$.
      Then $F$ is a map from $\kappa_{i}$ to $\lambda_{i}$.
      We have $\Delta(i) = \{ F(n) \mid n \in \kappa_{i} \}$.
      Thus $F[\kappa_{i}] = \Delta(i)$.
      Therefore $|\Delta(i)|
        = |F[\kappa_{i}]|
        \leq |\kappa_{i}|
        = \kappa_{i}
        < \lambda_{i}$.
      Indeed $|F[\kappa_{i}]| \leq |\kappa_{i}|$
      (by \cref{SET_THEORY_06_8113916590686208}).
      Indeed $\kappa_{i}$ and $\lambda_{i}$ are sets.
    End.

    Define $f(i) =$ ``choose an element $v$ of $\lambda_{i} \setminus
    \Delta(i)$ in $v$'' for $i \in D$.
    Indeed $\lambda_{i} \setminus \Delta(i)$ is nonempty for each $i \in D$.
    Then $f$ is an element of $\ProdSet{\lambda}{D}$.
    Take an element $j$ of $D$ and an element $m$ of $\kappa_{j}$ such that
    $G(m,j) = f$.
    $G(m,j)(j)$ is an element of $\Delta(j)$ and
    $f(j)$ is not an element of $\Delta(j)$.
    Contradiction.
  \end{proof}
\end{forthel}

\begin{thebibliography}{1}
  \bibitem{Koenig1905} Julius König,
  \textit{Zum Kontinuumsproblem};
  Mathematische Annalen 60 (1905)
\end{thebibliography}

\end{document}
