Commit 2024-07-28 19:58 03943935

feat: proper group actions (#11746) We define proper action of a group on a topological space, and we prove that in this case the quotient space is T2. We prove that if a Hausdorff group acts properly on $X$, then $X$ is Hausdorff. We also give equivalent definitions of proper action using ultrafilters and show the transfer of proper action to a closed subgroup. We show that if $X \times X$ is Hausdorff and compactly generated then the action is properly discontinuous if and only if it is continuous in the second variable and proper in the sense defined here. The "compactly generated" assumption is to be rephrased with typeclass inference in the future.