The action underlying a topological torsor is proper. #
instance
instProperSMul
{V : Type u_1}
{P : Type u_2}
[Group V]
[Torsor V P]
[TopologicalSpace V]
[TopologicalSpace P]
[IsTopologicalTorsor P]
:
ProperSMul V P
If P is a topological torsor over V, the action of V on P is proper.
instance
instProperVAdd
{V : Type u_1}
{P : Type u_2}
[AddGroup V]
[AddTorsor V P]
[TopologicalSpace V]
[TopologicalSpace P]
[IsTopologicalAddTorsor P]
:
ProperVAdd V P
If P is a topological additive torsor over V, the additive action of V on
P is proper.