Theorems · Theorem · manifolds

properlyDiscontinuousSMul_iff_properSMul

∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  [inst_3 : MulAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [DiscreteTopology G] [ContinuousConstSMul G X],
  ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

If a discrete group acts on a T2 space X such that X × X is compactly generated, and if the action is continuous in the second variable, then the action is properly discontinuous if and only if it is proper. This is in particular true if X is first-countable or weakly locally compact.

Defined in

Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Cited by

0 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceGroupTopologicalSpaceMulActionCompactlyGeneratedSpaceT2SpaceDiscreteTopologyContinuousConstSMul