Proper continuous maps of topological spaces

Let $X$ and $Y$ be topological spaces (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) and let $f:X\to Y$ be continuous (Continuity of a map of topological spaces at a point and globally). Then $f$ is proper when for every compact subset $K\subseteq Y$ (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) its preimage $f^{-1}(K)$ is a compact subset of $X$. Compactness of subsets is the intrinsic condition of Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, namely compactness of the subspace $f^{-1}(K)$ with the subspace topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace); by 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 it is equivalent to the ambient reading, so a subset is compact exactly when every cover by open subsets of the ambient space has a finite subcover, and the two readings are used interchangeably below without further comment.

This is the notion of properness used throughout the analytic six-operation development on this page, where the spaces involved are locally compact Hausdorff (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not). The stability properties consumed by the later items — closed inclusions are proper, composites of proper maps are proper, properness is preserved by base change along a continuous map into a Hausdorff space, and fibres and closed subspaces of a proper map inherit properness — are proved in the lemma lem-proper-continuous-map-stability on this page. The definition involves no choice principle: it quantifies over compact subsets and preimages only.