Commit 2023-06-28 10:21 52336fd7

feat(Topology/Algebra/Group/Basic): product of compact set and closed set is closed (#5471) Also adds the version for group actions, and the consequence that if we quotient by a compact subgroup then the quotient map is closed. I also made some syntax tweaks in some places, mainly making use of our great new implicit functions.