Solution (source code)

= Solution

The <Lie group> $PSL(2,\mathbb C)$ is a <second-countable space>. For every point of its discrete <subgroup>, choose the first basic neighbourhood isolating that point; different elements require different such neighbourhoods. This injects $G$ into a countable set, proving countability.

A discrete <subgroup> is closed and meets compact sets in finitely many points. Indeed, distinct <subgroup> elements accumulating anywhere would give quotients converging to identity, contradicting an identity neighbourhood containing no other <subgroup> element. To apply this, use the positive Hermitian determinant-one model of <hyperbolic space>. At the base point $I$, the image under a determinant-one representative $g$ is $gg^*$ and
$$
2\cosh d(I,gg^*)=\operatorname{tr}(gg^*)=\sum_{i,j}|g_{ij}|^2.
$$
This distance formula follows by unitary diagonalization: <eigenvalues> are $e^t,e^{-t}$ and the axial hyperbolic displacement is $|t|$. Thus bounded displacement bounds all matrix entries. The determinant-one condition is closed, so the resulting set is compact; the quotient by $\{I,-I\}$ is compact too. Conjugation gives the same conclusion at any base point. These are the <bounded displacement sets of hyperbolic isometries are compact> facts.

Hence, for each $R$, only finitely many $g\in G$ satisfy $d(p,gp)\le R$. Any enumeration of an infinite group without repetitions therefore has \b[$d(p,g_np)\to\infty$]. A finite discrete group is a harmless exception to the wording: it has no infinite enumeration of distinct elements, and proper discontinuity is immediate.

For a <compact set> $C$, put $R=\max_{x\in C}d(p,x)$. If $gC\cap C\ne\varnothing$, choose $x,gx\in C$. The triangle inequality gives $d(p,gp)\le d(p,gx)+d(x,p)\le2R$. Only finitely many such $g$ exist, proving <properly discontinuous group action>. Conversely, if the <subgroup> is not discrete, there are distinct $g_n\to e$. A closed ball about $p$ then meets its images under infinitely many $g_n$, violating this compact-set definition. Thus \b[discreteness is equivalent to proper discontinuity]. Here proper discontinuity allows finite point stabilizers; a stronger convention requiring freeness would exclude discrete elliptic subgroups and is not the equivalence intended.