Theorem MulAction.properSMul_iff_isCompact_setOf_inter_nonempty

Modification history

2026-03-24 19:17
Mathlib/Topology/Algebra/ProperAction/CompactlyGenerated.lean
feat(Topology/Algebra/ProperAction): Fiberwise criterion for ProperSMul (#36904) …
Added MulAction.properSMul_iff_isCompact_setOf_inter_nonemptyView on Github →