Theorem ProperSMul.isCompact_setOf_inter_nonempty

Modification history

2026-03-24 19:17

Mathlib/Topology/Algebra/ProperAction/Basic.lean

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

Added ProperSMul.isCompact_setOf_inter_nonempty View on Github →