Theorems · Theorem · manifolds

ProperSMul.isProperMap_smul_pair

∀ {G : Type u_1} {X : Type u_2} {inst : TopologicalSpace G} {inst_1 : TopologicalSpace X} {inst_2 : Group G}
  {inst_3 : MulAction G X} [self : ProperSMul G X], IsProperMap fun gx => (gx.1 • gx.2, gx.2)

Proper group action in the sense of Bourbaki: the map G × X → X × X is a proper map (see IsProperMap).

Defined in

Mathlib.Topology.Algebra.ProperAction.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

ProperSMul