Theorems · Theorem · manifolds

ProperVAdd.isProperMap_vadd_pair_set

∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperVAdd G X] {t : Set X}, IsProperMap fun gx => (gx.1 +ᵥ ↑gx.2, gx.2)

If G acts on X properly, then the map G × T → X × T, (g, t) ↦ (g +ᵥ t, t) is still proper for any subset T of X.

Defined in

Mathlib.Topology.Algebra.ProperAction.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionTopologicalSpaceTopologicalSpaceProperVAdd