Theorems · Theorem · manifolds

MulAction.properSMul_of_proper_orbitMap

∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ContinuousSMul G X] [IsTopologicalGroup G] [MulAction.IsPretransitive G X] {x : X},
  (IsProperMap fun g => g • x) → ProperSMul G X

If G acts transitively on X, and the orbit map of a point in X is a proper map, then the action is proper.

Defined in

Mathlib.Topology.Algebra.ProperAction.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulActionTopologicalSpaceTopologicalSpaceContinuousSMulIsTopologicalGroupMulAction.IsPretransitive