Commit 2024-07-19 06:14 a3695b98
View on Github →chore: Move universally closed characterisation of proper maps (#14848)
Did you know that we need the Stone-Čech compactification to talk about sum of continuous functions? Me neither!
Split Topology.ProperMap
into
Topology.Maps.Proper.Basic
for everything but the universally closed characterisation.Topology.Maps.Proper.UniversallyClosed
for the universally closed characterisation. Also moveTopology.Maps
toTopology.Maps.Basic
to match.