ThmDex – An index of mathematical definitions, results, and conjectures.

Proof P2747 on R4010: Polish space is first-countable

P2747

This result is a particular case of R610: Metrisable topological space is first-countable. $\square$