Commit 2022-01-25 17:30 6184db11

View on Github →

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.

Estimated changes

Modified src/group_theory/group_action/basic.lean

added theorem mul_action.image_inter_image_iff

added theorem mul_action.quotient_preimage_image_eq_union_mul

Modified src/topology/algebra/mul_action.lean

Created src/topology/algebra/mul_action2.lean

added def homeomorph.smul

added def homeomorph.vadd

added theorem is_open_map_quotient_mk_mul

Modified src/topology/separation.lean

added theorem t2_separation_compact_nhds

added theorem t2_separation_nhds

added theorem t2_space_iff_nhds

Modified src/topology/subset_properties.lean

added theorem local_compact_nhds