Rectangular neighborhood of a product of compact sets (source code)

= Rectangular neighborhood of a product of compact sets
{title2=$K\times L\subseteq U\times V\subseteq W$}

If $K$ and $L$ are <compact subsets> of two spaces and $W$ is an <open neighborhood> of their product, there are <open sets> $U,V$ with $K\times L\subseteq U\times V\subseteq W$. First use <compactness> of $L$ to produce a rectangle around each slice $\{x\}\times L$, intersecting finitely many first factors and uniting second factors. Then use <compactness> of $K$, uniting finitely many resulting first factors and intersecting second factors. No <Hausdorff> assumption is required.