Tube lemma: if $K$ is compact and an open $N \subseteq X \times Z$ contains $K \times \{z_0\}$, then $N$ contains $K \times W$ for some open $W \ni z_0$

Let $(X, \mathcal{T}_X)$ and $(Z, \mathcal{T}_Z)$ be topological spaces (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) and give $X \times Z$ the product topology (The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space). Let $K \subseteq X$ be a compact subset (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right), let $z_0 \in Z$, and let $N \subseteq X \times Z$ be open with

$K \times \{z_0\} \;\subseteq\; N .$

Then there is an open $W \subseteq Z$ with $z_0 \in W$ and

$K \times W \;\subseteq\; N .$

The set $K \times W$ is the tube of the name. The case $K = \varnothing$ is included and is settled by $W = Z$. No choice principle is used at all: the cover produced below is indexed by pairs of open sets, so the indexed form of the ambient compactness criterion (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, claim 2) returns the second entries together with the indices and nothing has to be selected afterwards.

What the lemma is for. It is the step that makes a product of two compact spaces compact (A product of finitely many compact spaces is compact in the product topology): a cover of $X \times Z$ restricted to the slice $X \times \{z_0\}$ can be thinned by compactness of $X$, and the tube lemma is what turns the resulting cover of the slice into a cover of a whole open band $X \times W$ around it. Compactness of $K$ is essential and cannot be weakened to closedness: an open set containing the slice over a non-compact $K$ need not contain any tube. Finiteness is what does the work — a union of finitely many basic boxes containing the slice always contains a tube, since intersecting the finitely many second factors that meet $z_0$ leaves an open $W \ni z_0$ — and it is compactness of $K$ that produces the finite subfamily.

Why the pairs are carried along. A proof that says "for each $x \in K$ choose open $U_x \ni x$ and $V_x \ni z_0$ with $U_x \times V_x \subseteq N$" has selected a pair for every point of $K$ at once, which for an arbitrary compact $K$ is the Axiom of Choice. Indexing the cover by the pairs themselves removes the selection: the compactness criterion hands back finitely many indices, and an index here already carries its own $V$.

A metric special case is stated elsewhere in the library, as lem-tube-lemma-for-a-compact-metric-factor, which assumes $X$ metric and carries the alias lem-tube-lemma; it is named here in plain text because its page comes after this one in the reading order. It is not used above, and the present lemma assumes nothing about $X$ beyond compactness of $K$.