Theorem properlyDiscontinuousSMul_iff_properSMul

Modification history

2026-03-24 19:17
Mathlib/Topology/Algebra/ProperAction/CompactlyGenerated.lean
feat(Topology/Algebra/ProperAction): Fiberwise criterion for ProperSMul (#36904) …
Modified properlyDiscontinuousSMul_iff_properSMulView on Github →
2024-10-14 12:17
Mathlib/Topology/Algebra/ProperAction/Basic.lean
feat: compactly generated spaces for proper maps and preimages of compact sets / proper and properly discontinuous actions (#15239) …
Modified properlyDiscontinuousSMul_iff_properSMulView on Github →
2024-07-28 19:58
Mathlib/Topology/Algebra/ProperAction.lean
feat: proper group actions (#11746) …
Added properlyDiscontinuousSMul_iff_properSMulView on Github →