Theorems · Theorem · manifolds

ProperVAdd.isCompact_setOfPred_inter_nonempty

∀ {X : Type u_2} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [inst_3 : TopologicalSpace G] [ProperVAdd 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 AddAction.properVAdd_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

TopologicalSpaceAddGroupAddActionTopologicalSpaceProperVAdd