Theorems · Theorem · manifolds

ProperSMul.isProperMap_smul_pair_set

∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperSMul 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

GroupMulActionTopologicalSpaceTopologicalSpaceProperSMul