Structures · Topology
ProperlyDiscontinuousSMul
Class ProperlyDiscontinuousSMul Γ T says that the scalar multiplication (•) : Γ → T → T
is properly discontinuous, that is, for any pair of compact sets K, L in T, only finitely many
γ : Γ move K to have nontrivial intersection with L.
- Defined in
- Mathlib.Topology.Algebra.ConstMulAction
- Shape
- 2 explicit arguments · adds finite_disjoint_inter_image
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self
- ProperlyDiscontinuousSMul.finite_disjoint_inter_image
- ProperlyDiscontinuousSMul.ofFiniteRelIndex
- ProperlyDiscontinuousSMul.finite_stabilizer'
- Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul
- Topology.IsQuotientMap.isQuotientCoveringMap_of_properlyDiscontinuousSMul
- isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul
- ProperlyDiscontinuousSMul.finite_stabilizer
- isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul
- MulAction.instChartedSpaceQuotient
- t2Space_of_properlyDiscontinuousSMul_of_t2Space
- instProperlyDiscontinuousSMulSubtypeMemSubgroup
- ProperlyDiscontinuousSMul.exists_nhds_disjoint_image
Ancestors0
No ancestors.