mathlib3

30f3788c - feat(topology/discrete_quotient): Discrete quotients of topological spaces (#7425)

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. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>