When a proper action is properly discontinuous

This file proves that if a discrete group acts on a T2 space X such that X × X is compactly coherent, 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.

Main statements

• properlyDiscontinuousSMul_iff_properSMul: If a discrete group acts on a T2 space X such that X × X is compactly coherent, and if the action is continuous in the second variable, then the action is properly discontinuous if and only if it is proper.
• MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty: if G is a topological group acting continuously on a T2 space X such that X × X is compactly coherent, then the action is proper iff, for each pair of compacts U, V ⊆ X, the set of g : G such that g • U intersects V is compact.

Tags

group action, proper action, properly discontinuous, compactly generated

theorem MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [Group G] [TopologicalSpace G] [MulAction G X] [CompactlyCoherentSpace (X × X)] [T2Space X] [ContinuousSMul G X] : ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g : G | (g • U ∩ V).Nonempty}

The G-action on X is proper iff, for each pair of compacts U, V in X, the set of g such that U intersects g • V is compact.

See ProperSMul.isCompact_setOfPred_inter_nonempty for a one-way implication with fewer conditions.

Note: We assume CompactlyCoherentSpace (X × X) as this is the minimal assumption needed to make the proof work; but this follows from various more familiar conditions, such as FirstCountableTopology X. Importing Mathlib.Topology.Sequences makes this implication available.

theorem AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddGroup G] [TopologicalSpace G] [AddAction G X] [CompactlyCoherentSpace (X × X)] [T2Space X] [ContinuousVAdd G X] : ProperVAdd G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g : G | ((g +ᵥ U) ∩ V).Nonempty}

The G-action on X is proper iff, for each pair of compacts U, V in X, the set of g such that U intersects g +ᵥ V is compact.

See ProperVAdd.isCompact_setOfPred_inter_nonempty for a one-way implication with fewer conditions.

Note: We assume CompactlyCoherentSpace (X × X) as this is the minimal assumption needed to make the proof work; but this follows from various more familiar conditions, such as FirstCountableTopology X. Importing Mathlib.Topology.Sequences makes this implication available.

@[deprecated MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty (since := "2026-07-09")]

theorem MulAction.properSMul_iff_isCompact_setOf_inter_nonempty {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [Group G] [TopologicalSpace G] [MulAction G X] [CompactlyCoherentSpace (X × X)] [T2Space X] [ContinuousSMul G X] : ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g : G | (g • U ∩ V).Nonempty}

Alias of MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty.

---

The G-action on X is proper iff, for each pair of compacts U, V in X, the set of g such that U intersects g • V is compact.

See ProperSMul.isCompact_setOfPred_inter_nonempty for a one-way implication with fewer conditions.

Note: We assume CompactlyCoherentSpace (X × X) as this is the minimal assumption needed to make the proof work; but this follows from various more familiar conditions, such as FirstCountableTopology X. Importing Mathlib.Topology.Sequences makes this implication available.

@[deprecated AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty (since := "2026-07-09")]

theorem AddAction.properVAdd_iff_isCompact_setOf_inter_nonempty {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddGroup G] [TopologicalSpace G] [AddAction G X] [CompactlyCoherentSpace (X × X)] [T2Space X] [ContinuousVAdd G X] : ProperVAdd G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g : G | ((g +ᵥ U) ∩ V).Nonempty}

Alias of AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty.

---

The G-action on X is proper iff, for each pair of compacts U, V in X, the set of g such that U intersects g +ᵥ V is compact.

See ProperVAdd.isCompact_setOfPred_inter_nonempty for a one-way implication with fewer conditions.

Note: We assume CompactlyCoherentSpace (X × X) as this is the minimal assumption needed to make the proof work; but this follows from various more familiar conditions, such as FirstCountableTopology X. Importing Mathlib.Topology.Sequences makes this implication available.

theorem properlyDiscontinuousSMul_iff_properSMul {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [Group G] [TopologicalSpace G] [MulAction G X] [CompactlyCoherentSpace (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 coherent, 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.

theorem properlyDiscontinuousVAdd_iff_properVAdd {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddGroup G] [TopologicalSpace G] [AddAction G X] [CompactlyCoherentSpace (X × X)] [T2Space X] [DiscreteTopology G] [ContinuousConstVAdd G X] : ProperlyDiscontinuousVAdd G X ↔ ProperVAdd G X

If a discrete additive 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.