Commit 2024-07-29 07:19 1d080245
View on Github →feat: Rename CompactlyGeneratedSpace to UCompactlyGeneratedSpace (#15201)
CompactlyGeneratedSpace is defined in Mathlib.Topology.Category.CompactlyGenerated. Due to functors considerations, the definition involves a free universe parameter, which is not desirable for topological purposes. Therefore we rename CompactlyGeneratedSpace to UCompactlyGeneratedSpace so that CompactlyGeneratedSpace can be defined as a special case. This was discussed here.