Quotient map to orbit space is a covering map

Stream: Is there code for X?

[Michael Rothgang]

Suppose a group G acts properly discontinuously on X. Mathlib knows that the quotient map X \to X/G is continuous. Does it also know this is a covering map?

[Michael Rothgang]

(I did loogle, and found, for example, that the quotient map is an OpenQuotientMap, or that a covering map is a local homeomorphism, but not this particular result. Indeed, loogling for ProperlyDiscontinuousSMul yields just 8 results.)

[Etienne Marion]

Don’t know if that helps but there is also docs#ProperSMul

[Michael Rothgang]

Thanks! I know about that also (and there are only 17 lemmas involving it, none of which seems relevant either).

[Anatole Dedecker]

There is a (quite old) open PR by @Junyan Xu about this

[Etienne Marion]

#7596

[Michael Rothgang]

Thanks; this is very helpful!

[Michael Rothgang]

#32681 splits out a file move from that PR