Positive orbit separation implies a Hausdorff quotient (source code)

= Positive orbit separation implies a Hausdorff quotient

Suppose a <group> acts by <isometries> on a <metric space> $X$, and for points $a,b$ in different <orbits> one has $\inf_g d(a,gb)>0$. Then the <orbit> space with its <quotient topology> is <Hausdorff>. Indeed, choose $\varepsilon$ less than one third of this positive infimum and saturate the <open> radius-$\varepsilon$ balls about $a$ and $b$ by the <action>. These saturated sets are <open> because every acting <isometry> is a <homeomorphism>. Their translates cannot meet: their centres stay at least the given positive <distance> apart. Their disjoint <open> images in the quotient separate the two <orbit> points, since the preimage of each image is its saturated set. This applies to the <glide reflection> $(x,y)\mapsto(x+1,-y)$ on a <closed> strip: the <distance> from one point to the translates of another tends to infinity as the <integer> translation grows, so two distinct <orbits> have a positive minimum <distance>.