Projection with a compact factor is closed (source code)

= Projection with a compact factor is closed
{title2=$X\text{ compact}\implies\pi_Y:X\times Y\to Y\text{ closed}$}

For <metric spaces> $X,Y$ with $X$ <compact>, the <projection with a compact factor is closed>: if $F\subset X\times Y$ is a <closed set> and $y_n\in\pi_Y(F)$ converges to $y$, choose $x_n$ with $(x_n,y_n)\in F$. <Sequential compactness> supplies $x_{n_k}\to x$, so $(x_{n_k},y_{n_k})\to(x,y)\in F$, proving $y\in\pi_Y(F)$. The <projection map> is also <continuous> for the sum <metric>. Without <compactness>, the <closed set> $\{(x,y)\in\mathbb R^2:xy=1\}$ projects to the nonclosed set $\mathbb R\setminus\{0\}$.