Theorems · Theorem · manifolds

ProperVAdd.isProperMap_vadd_pair

∀ {G : Type u_1} {X : Type u_2} {inst : TopologicalSpace G} {inst_1 : TopologicalSpace X} {inst_2 : AddGroup G}
  {inst_3 : AddAction G X} [self : ProperVAdd 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

ProperVAdd