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 move Topology.Maps to Topology.Maps.Basic to match.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/ProperConstSMul.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

Renamed Mathlib/Topology/Maps.lean to Mathlib/Topology/Maps/Basic.lean

Renamed Mathlib/Topology/ProperMap.lean to Mathlib/Topology/Maps/Proper/Basic.lean

deleted theorem isProperMap_iff_isClosedMap_ultrafilter

deleted theorem isProperMap_iff_universally_closed

Created Mathlib/Topology/Maps/Proper/UniversallyClosed.lean

added theorem isProperMap_iff_isClosedMap_ultrafilter

added theorem isProperMap_iff_universally_closed

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean