Theorems · Theorem · manifolds

MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty

∀ {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] [ContinuousSMul G X],
  ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {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.

Defined in

Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupTopologicalSpaceMulActionCompactlyGeneratedSpaceT2SpaceContinuousSMul