# Commit 2020-07-06 07:16 5ff099b6

View on Github →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`