\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{closed-projection characterization of compactness}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{topology}{}\paragraph*{{Topology}}\label{topology}

[[!include topology - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{statement_and_proof}{Statement and proof}\dotfill \pageref*{statement_and_proof} \linebreak
\noindent\hyperlink{variant_proofs}{Variant proofs}\dotfill \pageref*{variant_proofs} \linebreak
\noindent\hyperlink{consequences}{Consequences}\dotfill \pageref*{consequences} \linebreak
\noindent\hyperlink{TychonoffTheorem}{Tychonoff theorem}\dotfill \pageref*{TychonoffTheorem} \linebreak
\noindent\hyperlink{TubeLemma}{Tube lemma}\dotfill \pageref*{TubeLemma} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{statement_and_proof}{}\subsection*{{Statement and proof}}\label{statement_and_proof}

There are a number of [[category theory|categorically-flavored]] ways of characterizing [[compact spaces]]; for example, as [[relational beta-modules]] $X$ where the beta-module structure $\xi: \beta(X) \nrightarrow X$ is an [[entire relation]] (satisfies $1_{\beta(X)} \leq \xi^\circ \xi$). One of the more useful characterizations, as emphasized by [[Walter Tholen]], is given by the following elementary statement (also one of the definitions listed in [[compact space]]):

\begin{theorem}
\label{char}\hypertarget{char}{}
A [[topological space]] $X$ is [[compact topological space|compact]] if and only if for every space $Y$, the [[projection map]] $\pi \colon Y \times X \to Y$ out of the [[product topological space]] is a [[closed map]].

\end{theorem}
In this article we will collect a number of proofs and points of view on this result, and show how it makes possible a very direct hands-on proof of the [[Tychonoff theorem]], without the need for infrastructure such as [[ultrafilters]] or [[nets]]. This type of proof may be adapted for use in undergraduate classrooms.

The ``only if'' half is covered in essentially every textbook and should be routine for any working mathematician, although it seems proofs often use needlessly many indices and look as though they tacitly invoke the [[axiom of choice]]. Our proof should help circumvent that impression.

\begin{prop}
\label{onlyif}\hypertarget{onlyif}{}
If $X, Y$ are [[topological spaces]] with $X$ [[compact topological space|compact]], then the [[projection map]] $\pi \colon Y \times X \to Y$ out of the [[product topological space]] is a [[closed map]].

\end{prop}
\begin{proof}
Let $C \subseteq Y \times X$ be a [[closed subset]]; we must show the [[direct image]] $\pi(C)$ is closed in $Y$. Suppose $y \notin \pi(C)$; equivalently, suppose that the [[pre-image]] $\pi^{-1}(y) = \{y\} \times X$ does not intersect $C$. By the nature of closed subsets (\href{Introduction+to+Topology+--+1#UnionOfOpensGivesClosure}{this lemma}) it is sufficient that we find an [[open neighborhood]] $V$ of $y$ that does not [[intersection|intersect]] $\pi(C)$, or equivalently such that $(V \times X) \cap C = \emptyset$. Consider the collection of all open $U \subseteq X$ such that $(W \times U) \cap C = \emptyset$ for some [[open neighborhood]] $W$ of $y$. This collection [[open cover|covers]] $X$, since $(y, x) \notin C$ for every $x \in X$ and by closure of $C$ we can therefore find a neighborhood $W \times U$ of $(y, x)$ that doesn't intersect $C$. By compactness of $X$, this [[open cover]] has a [[finite cover|finite]] subcover, say $U_1, \ldots, U_n$. For each of these $U_i$ there is a corresponding $W_i$ such that $(W_i \times U_i) \cap C = \emptyset$ (in fact there is a unique largest such $W_i$: just take the union of all such). Now put $V \coloneqq \bigcap_{i=1}^n W_i$. We have for each $i$ between $1$ and $n$ that $V \times U_i \subseteq W_i \times U_i \subseteq \neg C$ (the [[complement]] of $C$ in $X \times Y$), hence

\begin{displaymath}
V \times X \;=\; V \times \bigcup_{i=1}^n U_i \;=\; \bigcup_{i=1}^n V \times U_i \subseteq \neg C
\end{displaymath}
so that $(V \times X) \cap C = \emptyset$.

\end{proof}
The ``if'' half is not quite so routine. We will first give a very direct proof that doesn't involve any fancy machinery (such as [[ultrafilters]]), although the fancy machinery does help give a better conceptual understanding of what is really going on, as we explain below.

\begin{prop}
\label{if}\hypertarget{if}{}
If $X$ is a [[topological space]] with the property that the [[projection]] $\pi \colon Y \times X \to Y$ out of the [[product topological space]] is a [[closed map]] for every space $Y$, then $X$ is [[compact topological space|compact]].

\end{prop}
\begin{proof}
Given a space $X$ satisfying this property, let $(C_i)_{i \in I}$ be any collection of [[closed subsets]] of $X$ having the [[finite intersection property]], that any intersection of finitely many $C_i$ is [[inhabited set|inhabited]]. Compactness of $X$ will follow if we can show $\bigcap_{i \in I} C_i$ is inhabited (by \href{compact+space#fip}{this prop.}).

Given that collection, construct a space $Y$ whose underlying set ${|Y|}$ is formed by adjoining a point $\infty$ to the underlying set of $X$ (so ${|Y|} = {|X|} \sqcup \{\infty\}$), and topologized by taking [[sub-base of a topology|subbasis]] elements to consist of \emph{any} subset of $X$ (not necessarily open) and any subset of the form $C_i \cup \{\infty\}$. (Thus we are embedding the ``[[discrete topological space|discretification]]'' of $X$ in a larger space $Y$.) Let $K \subseteq Y \times X$ be the [[topological closure]] of the set $\Delta = \{(x, x): x \in {|X|}\}$. By hypothesis, $\pi(K)$ is closed in $Y$, and contains $X$. But then it must also contain $\infty$ because the [[finite intersection property]] of the collection $(C_i)$ guarantees that $\infty$ is not an [[open point]] of $Y$. It follows that $K$ contains a point of the form $(\infty, x)$.

This means that every [[neighborhood]] $(C_i \cup \{\infty\}) \times U$ of $(\infty, x)$ intersects the [[diagonal]] $\Delta$ in an inhabited set. In other words, $C_i \cap U$ is inhabited. But this means that $x \in C_i$ for every $i$, for if $x \notin C_i$ for some $i$, then by closure of $C_i$ we could find an open neighborhood $U$ of $x$ such that $C_i \cap U = \emptyset$. Hence $x \in \bigcap_{i \in I} C_i$, making this intersection inhabited, as required.

\end{proof}
\begin{remark}
\label{Acknowledgement}\hypertarget{Acknowledgement}{}
I ([[Todd Trimble]]) learned of this particular arrangement of proof during an email exchange with [[Tom Leinster]], who told me he learned it from [[Ioan James]]. I don't know who first invented it though. Pedagogically it is attractive because it avoids any need to discuss nets or ultrafilters or filters; it's just straight-up topology of the kind taught at typical American undergraduate institutions.

\end{remark}
\hypertarget{variant_proofs}{}\subsubsection*{{Variant proofs}}\label{variant_proofs}

There are actually quite a few proofs of Proposition \ref{if} that appear in the literature. The proof given \hyperlink{ifProof}{above} might have been the result of a gradual whittling down from more abstract, high-powered-looking proofs.

\begin{enumerate}%
\item One ``canonical'' proof that a seasoned mathematician might dream up goes as follows. Consider $Y = \beta({|X|})$, the space of [[ultrafilters]] on the underlying set ${|X|}$ of $X$, or the [[Stone-Cech compactification]] of $X$ (retopologized as a discrete space). Let $K \subseteq Y \times X$ be the convergence relation (i.e., $(U, x) \in K$ iff the ultrafilter $U$ on the set $X$ converges to the point $x$ in the space $X$). One readily checks that $K$ is closed. Thus $\pi(K) \subseteq Y$ is closed by hypothesis. Also observe that the ``diagonal'' $\Delta = \{(prin(x), x): x \in X\}$, where $prin(x)$ is the principal ultrafilter generated by $x$, sits inside $K$ since $prin(x)$ converges to $x$. So $\pi(K)$ also contains all principal ultrafilters which form a dense subset of $Y$. Being closed and dense, $\pi(K)$ is all of $Y$. But this just means that for every ultrafilter $U$ there is some $(U, x) \in K$, i.e., every ultrafilter converges to some point. This classically implies compactness of $X$.


\item On reflection, we didn't really have to consider the entire space $\beta({|X|})$; we can just work with one ultrafilter at a time. So if we want to prove that every ultrafilter $U$ converges, we can just look at the subset ${|X|} \cup \{U\} \hookrightarrow \beta({|X|})$ with the [[subspace topology]] coming from $\beta({|X|})$ and run through the same diagonal proof. This gives us the proof found in Bourbaki's General Topology: given an ultrafilter $U$ on the underlying set of $X$, form a new space $Y$ whose underlying set is ${|X|} \sqcup \{\infty\}$ and topologized by saying all subsets of $X$ are open, and $A \sqcup \{\infty\}$ is an open neighborhood of $\infty$ if $A \in U$. This is just a direct description of the subspace topology coming from $\beta({|X|})$, and the rest of the proof runs parallel to the proof given in 1.


\item On further reflection, the ultrafilter convergence characterization of compact spaces does rely on the [[ultrafilter theorem]] (that every proper filter can be extended to an ultrafilter), which involves the [[axiom of choice]] or some choice-y principle outside ZF. If one doesn't like this, one can always use just [[filters]] instead, and use the characterization of compact spaces that says that every proper filter on ${|X|}$ admits a [[cluster point]]. This characterization doesn't require any form of Choice. So, one would start with $Y = {|X|} \sqcup \{\infty\}$ but use a given proper filter $F$ to describe the neighborhoods of $\infty$; otherwise the description of $Y$ looks just the same as before.


\item On still further reflection, one doesn't have to mention filters or cluster points at all. Instead one can work directly with a collection of sets $C_i$ satisfying the finite intersection property, and secretly think of that as generating a filter (a proper one by the FIP) and then follow 3. to define the topology of the space $Y$. As it happens, a cluster point of that filter is just a point lying in the intersection of all the $C_i$. This brings us to the proof we gave of Proposition \ref{if}.


\item Still other clever constructions of $Y$ are available. One has been described by [[Martín Escardó]] (\href{Escardo09}{Escard\'o{} 09}), who credits [[Leopoldo Nachbin]]. One nice feature is that Escard\'o{} favors a point of view where instead of defining a continuous map $f: X \to Z$ to be closed if the direct image mapping or [[existential quantification]] $\exists_f: P(X) \to P(Z)$ preserves closed subsets, he uses instead the [[universal quantification]] $\forall_f: P(X) \to P(Z)$ and asks that this preserve \emph{open sets}. This strategy circumvents the apparent use of [[excluded middle]] in proving Proposition \ref{onlyif}: he proves it directly and constructively. In any case, he considers a [[directed set|directed]] [[open cover]] $\Sigma$ of the given space $X$, then takes $Y = \mathcal{O}(X)$, the set of open sets of $X$, and topologizes $Y$ by taking its inhabited open sets to be upward-closed subsets $W \subseteq \mathcal{O}(X)$ such that $W \cap \Sigma$ is inhabited. Using the open-set formulation of closed maps, he then argues that $X$ belongs to $\Sigma$, which proves compactness. (This argument was also reprised \href{https://ncatlab.org/toddtrimble/published/Characterizations+of+compactness#escardo}{here}.)



\end{enumerate}
\hypertarget{consequences}{}\subsection*{{Consequences}}\label{consequences}

\hypertarget{TychonoffTheorem}{}\subsubsection*{{Tychonoff theorem}}\label{TychonoffTheorem}

It has been observed by \hyperlink{CT1996}{Clementino and Tholen} that the closed-projection formulation of compactness (theorem \ref{char}) allows a fairly efficient proof of the [[Tychonoff theorem]], saying that the [[product topological space]] of any [[set]] of [[compact topological space]] is itself compact. First a very routine lemma.

\begin{lemma}
\label{LemmaTychonoff}\hypertarget{LemmaTychonoff}{}
Let $(X_i)_{i: I}$ be a family of [[topological spaces]]. Then for a point $x$ and subset $A$ of the [[product topological space]] $\prod_{i: I} X_i$, we have $x \in Cl(A)$ (the [[topological closure]] of $x$) if, for every [[finite set|finite]] $F \subseteq I$, we have $\pi_F(x) \in Cl(\pi_F(A))$ under the [[projection]] map $\pi_F \colon \prod_{i: I} X_i \to \prod_{i: F} X_i$.

\end{lemma}
\begin{proof}
Suppose $x \notin Cl(A)$, so that there is an [[open neighborhood]] $U$ of $x$ such that $U \cap A = \emptyset$ (by \href{Introduction+to+Topology+--+1#UnionOfOpensGivesClosure}{this lemma}). Sets of the [[pre-image]] of the form $\pi_i^{-1}(U_i)$ for open $U_i \subseteq X_i$ form a [[subbase|subbasis]] of the product topology, so there is a basis element $\pi_F^{-1}(V)$ (for some $V = U_{i_1} \times \ldots \times U_{i_n}$ and $F = \{i_1, \ldots, i_n\}$) that is a neighborhood of $x$ and contained in $U$, so we have $A \cap \pi_F^{-1}(V) = \emptyset$ or $A \subseteq \neg \pi_F^{-1}(V) = \pi_F^{-1}(\neg V)$ ([[pre-image]] of the [[complement]]) or what is the same, $\pi_F(A) \subseteq \neg V$ or $\pi_F(A) \cap V = \emptyset$. Since $V$ is a neighborhood of $\pi_F(x)$ not intersecting $\pi_F(A)$, we conclude $\pi_F(x) \notin Cl(\pi_F(A))$. In summary we have shown that $(x \notin Cl(A)) \Rightarrow \underset{ {F \subset  I} \atop { \text{finite} }}{\exists} \left( \pi_F(x) \notin Cl(\pi_F(A))\right)$. By [[contraposition]], this proves the claim.

\end{proof}
\begin{theorem}
\label{}\hypertarget{}{}
\textbf{([[Tychonoff theorem]])}

The [[cartesian product]] of a [[small set|small]] family of [[compact topological spaces]] with the [[product topology]] is itself compact.

\end{theorem}
\begin{proof}
Let $(X_\alpha)_{\alpha \lt \kappa}$ be a family of compact spaces indexed by an [[ordinal]] $\kappa$. According to Theorem \ref{char}, it is enough to show that the [[projection]]

\begin{displaymath}
Y \times \prod_{\alpha \lt \kappa} X_\alpha \to Y
\end{displaymath}
is a [[closed map]] for any space $Y$. We do this by [[induction]] on $\kappa$. The case $\kappa = 0$ is trivial.

It will be convenient to introduce some notation. For $\gamma \leq \kappa$, let $X^\gamma$ denote the product $Y \times \prod_{\alpha \lt \gamma} X_\alpha$ (so $X^0 = Y$ in this notation), and for $\beta \leq \gamma$ let $\pi_\beta^\gamma \;\colon\; X^\gamma \to X^\beta$ be the obvious projection map. Let $K \subseteq X^\kappa$ be closed, and put $K_\beta \coloneqq Cl(\pi_{\beta}^\kappa(K))$. In particular $K_\kappa = K$ since $K$ is closed, and we are done if we show $\pi_0^\kappa(K) = K_0$.

Assume as inductive hypothesis that starting with any $x_0 \in K_0$ there is $x_\beta \in K_\beta$ for all $\beta \lt \kappa$ such that whenever $\beta \lt \gamma \lt \kappa$, the compatibility condition $\pi_\beta^\gamma(x_\gamma) = x_\beta$ holds. In particular, $\pi_0^\beta(x_\beta) = x_0$ for all $\beta \lt \kappa$, and we are now trying to extend this up to $\kappa$.

If $\kappa = \beta + 1$ is a [[successor ordinal]], then the projection

\begin{displaymath}
\pi_\beta^\kappa \;\colon\; X^\beta \times X_\beta \to X^\beta
\end{displaymath}
is a closed map since $X_\beta$ is compact. Thus $\pi_\beta^\kappa(K) = Cl(\pi_\beta^\kappa(K)) = K_\beta$ since $K$ is closed, so there exists $x_\kappa \in K$ with $\pi_\beta^\kappa(x_\kappa) = x_\beta$, and then

\begin{displaymath}
\pi_0^\kappa(x_\kappa) = \pi_0^\beta \pi_\beta^\kappa (x_\kappa) = \pi_0^\beta(x_\beta) = x_0
\end{displaymath}
as desired.

If $\kappa$ is a [[limit ordinal]], then we may regard $X^\kappa$ as the [[inverse limit]] of spaces $(X^\beta)_{\beta \lt \kappa}$ with the obvious transition maps $\pi_\beta^\gamma$ between them. Hence the tuple $(x_\beta)_{\beta \lt \kappa}$ defines an element $x_\kappa$ of $X^\kappa$, and all that remains is to check that $x_\kappa \in K$. But since $K$ is closed, lemma \ref{LemmaTychonoff} says that it is sufficient to check that for every finite set $F$ of ordinals below $\kappa$, that $\pi_F(x_\kappa) \in Cl(\pi_F(K))$ (as a subspace of $\prod_{\alpha \in F} X_\alpha$). But for every such $F$ there is some $\beta \lt \kappa$ that dominates all the elements of $F$. One then checks

\begin{displaymath}
\pi_F(x_\kappa) = \pi_F^\beta \pi_\beta^\kappa(x_\kappa) = \pi_F^\beta(x_\beta) \in \pi_F^\beta(K_\beta) = \pi_F^\beta(Cl(\pi_\beta^\kappa(K))) \subseteq Cl(\pi_F^\beta \pi_\beta^\kappa(K)) = Cl(\pi_F(K))
\end{displaymath}
where the inclusion indicated as $\subseteq$ just results from continuity of $\pi_F^\beta$. This completes the proof.

\end{proof}
\hypertarget{TubeLemma}{}\subsubsection*{{Tube lemma}}\label{TubeLemma}

The following useful lemma was effectively proved already within the proof of prop. \ref{onlyif}, but it is worth making it explicit:

\begin{lemma}
\label{tube}\hypertarget{tube}{}
\textbf{([[tube lemma]])}

Let

\begin{enumerate}%
\item $X$ be a [[topological space]],


\item $Y$ a [[compact topological space]],


\item $x \in X$ a point,


\item $W \underset{\text{open}}{\subset} X \times Y$ an open subset in the [[product topology]],



\end{enumerate}
such that the $Y$-[[fiber]] over $x$ is contained in $W$:

\begin{displaymath}
\{x\} \times Y \;\subseteq\; W
  \,.
\end{displaymath}
Then there exists an [[open neighborhood]] $U_x$ of $x$ such that the ``tube'' $U_x \times Y$ around the fiber $\{x \} \times Y$ is still contained:

\begin{displaymath}
U_x \times Y \subseteq W
  \,.
\end{displaymath}
\end{lemma}
\begin{proof}
Let

\begin{displaymath}
C \coloneqq (X \times Y) \backslash W
\end{displaymath}
be the [[complement]] of $W$. Since this is closed, by prop. \ref{onlyif} also its projection $p_X(C) \subset X$ is closed.

Now

\begin{displaymath}
\begin{aligned}
    \{x\} \times Y \subset W
      & \;\Leftrightarrow\;
    \{x\} \times Y \; \cap \; C = \emptyset  
    \\
    & \;\Rightarrow\; 
    \{x\} \cap  p_X(C) = \emptyset
  \end{aligned}
\end{displaymath}
and hence by the closure of $p_X(C)$ there is (by \href{Introduction+to+Topology+--+1#UnionOfOpensGivesClosure}{this lemma}) an open neighbourhood $U_x \supset \{x\}$ with

\begin{displaymath}
U_x \cap p_X(C) = \emptyset
  \,.
\end{displaymath}
This means equivalently that $U_x \times Y \cap C = \emptyset$, hence that $U_x \times Y \subset W$.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
More [[category theory|category theoretically]], the tube lemma \ref{tube} becomes the statement that for $X$ compact, the map $\forall_\pi: P(Y \times X) \to P(Y)$ takes opens to opens, as mentioned \hyperlink{StillOtherCleverConstructions}{above}.

\end{remark}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Maria Manuel Clementino]] and [[Walter Tholen]], \emph{Tychonoff's theorem in a category}, Proc. Amer. Math. Soc., Vol. 124 No. 11 (Nov. 1996), 3311-3314. (\href{http://www.ams.org/journals/proc/1996-124-11/S0002-9939-96-03435-1/S0002-9939-96-03435-1.pdf}{pdf})


\item [[Martín Escardó]], \emph{Intersections of compactly many open sets are open}, preprint dated May 27, 2009. (\href{http://www.cs.bham.ac.uk/~mhe/papers/compactness-submitted.pdf}{pdf})


\item [[James Milne]], section 17 of \emph{[[Lectures on Étale Cohomology]]}



\end{itemize}
Much of the material of the present article was earlier collected in

\begin{itemize}%
\item [[Todd Trimble]], \emph{Characterizations of compactness}, personal nLab webpage. (\href{https://ncatlab.org/toddtrimble/published/Characterizations+of+compactness}{link})

\end{itemize}


\end{document}