Theorem ProperSMul.isProperMap_smul_pair_set

Modification history

2025-11-05 17:11
Mathlib/Topology/Algebra/ProperAction/Basic.lean
feat: generalize `IsClosed.vadd_right_of_isCompact` to proper actions (#29715) …
Added ProperSMul.isProperMap_smul_pair_setView on Github →