English
A proper map is universally closed: for any topological space Z, the product map f × id: X × Z → Y × Z is closed.
Русский
Пропорное отображение является универсально замкнутым: для любого пространства Z отображение f × id: X × Z → Y × Z замкнуто.
LaTeX
$$$\\forall Z\\; [TopologicalSpace\\;Z],\\; IsClosedMap(Prod.map(f, id) : X \\times Z \\to Y \\times Z)$$$
Lean4
/-- A proper map `f : X → Y` is **universally closed**: for any topological space `Z`, the map
`Prod.map f id : X × Z → Y × Z` is closed. We will prove in `isProperMap_iff_universally_closed`
that proper maps are exactly continuous maps which have this property, but this result should be
easier to use because it allows `Z` to live in any universe. -/
theorem universally_closed (Z) [TopologicalSpace Z] (h : IsProperMap f) : IsClosedMap (Prod.map f id : X × Z → Y × Z) :=
-- `f × id` is proper as a product of proper maps, hence closed.
(h.prodMap isProperMap_id).isClosedMap
