Commit 2021-05-02 04:27 30f3788c

feat(topology/discrete_quotient): Discrete quotients of topological spaces (#7425) This PR defines the type of discrete quotients of a topological space and provides a basic API. In a subsequent PR, this will be used to show that a profinite space is the limit of its finite quotients, which will be needed for the liquid tensor experiment.