Theorems · Theorem · manifolds

ProperSMul.isCompact_setOfPred_inter_nonempty

∀ {X : Type u_2} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : Group G] [inst_2 : MulAction G X]
  [inst_3 : TopologicalSpace G] [ProperSMul G X] {U V : Set X},
  IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}

If G acts properly on X, then for each pair of compacts U, V ⊆ X, the set of g such that g • U intersects V is compact. See MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty for the two-way implication under additional conditions on G and X.

Defined in

Mathlib.Topology.Algebra.ProperAction.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupMulActionTopologicalSpaceProperSMul