English
A map is proper iff it is continuous and, for every space Z, the map f × id: X × Z → Y × Z is closed.
Русский
Отображение пропорно тогда и только тогда, когда оно непрерывно и для каждого пространства Z отображение \(f×id:X×Z→Y×Z\) замкнуто.
LaTeX
$$IsProperMap f \\iff Continuous f ∧ ∀ Z [TopologicalSpace Z], IsClosedMap (Prod.map f id : X × Z → Y × Z)$$
Lean4
/-- 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]. -/
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) [TopologicalSpace Z], IsClosedMap (Prod.map f id : X × Z → Y × Z) :=
by
constructor <;> intro H
· exact ⟨H.continuous, fun Z ↦ H.universally_closed _⟩
· rw [isProperMap_iff_isClosedMap_ultrafilter]
exact ⟨H.1, H.2 _⟩
