Definition 0.1. Let G be a topological group regarded as a topological space. Then G is
defined to be a Polish group if it is also a Polish space.
References
[1] Howard Becker, Alexander S. Kechris. 1996. The Descriptive Set Theory of Polish
Group Actions Cambridge University Press: Cambridge, UK, p.14.