Continuous actions of compact groups are proper

A continuous action of a compact group G on a Hausdorff space X is proper: the map (g, x) ↦ (g • x, x) is proper because its first coordinate ranges over a compact space. In particular the orbit space X ⧸ G is Hausdorff (t2Space_quotient_mulAction_of_properSMul), which is how quotients such as complex projective space, the orbit space of the circle acting on an odd sphere, are shown to be Hausdorff.

Main results

• TauCeti.properSMul_of_compactSpace: a continuous action of a compact group on a Hausdorff space is proper.

theorem TauCeti.properSMul_of_compactSpace (G : Type u_1) (X : Type u_2) [Group G] [TopologicalSpace G] [CompactSpace G] [MulAction G X] [TopologicalSpace X] [T2Space X] [ContinuousSMul G X] : ProperSMul G X

A continuous action of a compact group on a Hausdorff space is proper. This is not an instance, since ProperSMul itself provides ContinuousSMul.