The action underlying a topological additive torsor 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 torsor over V, the action of V on P is proper.