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`
