Theorem IsClosed.smul_left_of_isCompact

Modification history

2023-06-28 10:21
Mathlib/Topology/Algebra/Group/Basic.lean
feat(Topology/Algebra/Group/Basic): product of compact set and closed set is closed (#5471) …
Added IsClosed.smul_left_of_isCompactView on Github →