A map is proper iff it is continuous and universally closed

theorem isProperMap_iff_isClosedMap_ultrafilter {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)

A map f : X → Y is proper if and only if it is continuous and the map (Prod.map f id : X × Ultrafilter X → Y × Ultrafilter X) is closed. This is stronger than isProperMap_iff_universally_closed since it shows that there's only one space to check to get properness, but in most cases it doesn't matter.

theorem isProperMap_iff_universally_closed {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

A map f : X → Y is proper if and only if it is continuous and universally closed, in the sense that for any topological space Z, the map Prod.map f id : X × Z → Y × Z is closed. Note that Z lives in the same universe as X here, but IsProperMap.universally_closed does not have this restriction.

This is taken as the definition of properness in [N. Bourbaki, General Topology][bourbaki1966].