Commit 2024-10-14 12:17 8cb678e9

feat: compactly generated spaces for proper maps and preimages of compact sets / proper and properly discontinuous actions (#15239) Prove that a continuous function whose codomain is T2 and compactly generated is proper if and only if the preimages of compact sets are compact. This result already existed but was stated without the typeclass CompactlyGeneratedSpace. It is moved to its own file. When X \times X is T2 and compactly generated, a group action is proper if and only if it is properly discontinuous. This was stated without a type class instance for the compactly generated hypothesis. Now it is.