Theorems · Inductive type · manifolds

ProperSMul

(G : Type u_1) →
  (X : Type u_2) → [TopologicalSpace G] → [TopologicalSpace X] → [inst : Group G] → [MulAction G X] → Prop

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

14 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceGroupMulAction