Theorem MulAction.properSMul_of_proper_orbitMap

Modification history

2026-03-24 19:17

Mathlib/Topology/Algebra/ProperAction/Basic.lean

feat(Topology/Algebra/ProperAction): Fiberwise criterion for ProperSMul (#36904) …

Added MulAction.properSMul_of_proper_orbitMap View on Github →