mathlib3

6184db11 - feat(topology/algebra/mul_action2): quotient by a properly discontinuous group action is t2 (#10465)

feat(topology/algebra/mul_action2): quotient by a properly discontinuous group action is t2 (#10465) We prove that the quotient of a Hausdorff (t2) locally compact space by a properly discontinuous group action is itself Hausdorff. Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Eric <ericrboidi@gmail.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>