Commit 2025-10-18 20:17 9af14e50
View on Github →chore: move isProperMap_iff_isClosedMap_filter next to the ultrafilter version (#30409)
I don't quite know/remember what the motivation for having Mathlib.Topology.Maps.Proper.UniversallyClosed be a separate file, but certainly isProperMap_iff_isClosedMap_filter and isProperMap_iff_isClosedMap_ultrafilter should be together.