Compact-preimage theorem for closed maps (source code)

= Compact-preimage theorem for closed maps

Let $f:X\to Y$ be a <continuous map> that is a <closed map> and whose fibres are <compact>. Then $f^{-1}(K)$ is <compact> for every <compact set> $K\subseteq Y$, without a <Hausdorff> hypothesis. Given an <open cover>, cover each fibre by a finite union $V_y$ of its members. The set $W_y=Y\setminus f(X\setminus V_y)$ is open, contains $y$, and has $f^{-1}(W_y)\subseteq V_y$. A finite subcover of $K$ by the $W_y$ uses only finitely many original cover members and covers $f^{-1}(K)$. Empty fibres cause no exception.