Structures · Topology
ProperSMul
Proper group action in the sense of Bourbaki:
the map G × X → X × X is a proper map (see IsProperMap).
- Shape
- 2 explicit arguments · adds isProperMap_smul_pair
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Matrix.SpecialLinearGroup
- Subtype
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by10
- ProperSMul.isProperMap_smul_pair
- ProperSMul.isCompact_setOfPred_inter_nonempty
- ProperSMul.isProperMap_smul_pair_set
- ProperSMul.isCompact_setOf_inter_nonempty
- t2Space_of_properSMul_of_t1Group
- instProperSMulSubtypeMemSubgroupOfIsClosedCoe
- ProperSMul.toContinuousSMul
- t2Space_quotient_mulAction_of_properSMul
- properSMul_of_isClosedEmbedding
- IsClosed.smul_right_of_isCompact
Ancestors0
No ancestors.