Separation of a point and a compact set (source code)

= Separation of a point and a compact set
{title2=$x\notin K\ \Longrightarrow\ x\in V,\ K\subseteq U,\ U\cap V=\varnothing$}

In a <Hausdorff space>, a point $x$ outside a <compact subset> $K$ can be separated from all of $K$ by <disjoint> <open sets>. Choose <disjoint> <open neighbourhoods> $U_k$ of $k$ and $V_k$ of $x$ for each $k\in K$. Finitely many $U_k$ cover $K$ by <compactness>. Their <union> and the matching finite <intersection> of the $V_k$ give the displayed separation. If $K$ is empty, choose $U=\varnothing$, $V=X$. Thus $X\setminus K$ is <open>, proving that $K$ is <closed>.