Theorems · Theorem · manifolds

AddAction.properVAdd_of_proper_orbitMap

∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ContinuousVAdd G X] [IsTopologicalAddGroup G] [AddAction.IsPretransitive G X] {x : X},
  (IsProperMap fun g => g +ᵥ x) → ProperVAdd G X

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

AddGroupAddActionTopologicalSpaceTopologicalSpaceContinuousVAddIsTopologicalAddGroupAddAction.IsPretransitive