Commit 2020-07-06 07:16 5ff099b6

feat(topology): preliminaries for Haar measure (#3194) Define group operations on sets Define compacts, in a similar way to opens Prove some "separation" properties for topological groups Rename continuous.comap to opens.comap (so that we can have comaps for other kinds of sets in topological spaces) Rename inf_val to inf_def (unused) Move some definitions from topology.opens to topology.compacts