fintype of surjective

Stream: Is there code for X?

[Adam Topaz]

Does mathlib know that when $X$ is compact, $B$ is discrete and $\pi : X \to B$ is a surjective continuous map, that $B$ is a fintype?

[Johan Commelin]

Probably not in that combination. But I think all the ingredients are there.

[Johan Commelin]

I think there is some form of fintype_of_discrete_of_compact.

[Johan Commelin]

docs#fintype_of_compact_of_discrete

[Adam Topaz]

Thanks!