# Why is this function, used to show that finite Borel relations are smooth, Borel?

I'm reading a proof that all finite equivalence relations are smooth, which goes as follows:

Let $$E$$ be a finite Borel equivalence relation on a Polish space, we want to find a Borel function $$f\colon X\to X$$ reducing $$E$$ to $$\mathrm{Id}_X$$. Let $$<$$ be a Borel total order on $$X$$ and define $$f(x)$$ to be the $$<$$-least element of $$[x]_E$$.

Clearly $$xEy\iff f(x)=f(y)$$, but it's not clear to me why $$f$$ is Borel. I'm trying to argue that $$f^{-1}([x,\infty))$$ is Borel for all $$x\in X$$, but I can only show that is $$\mathbf{\Pi}^1_1$$ and I'm not seeing why it must be $$\mathbf{\Sigma}^1_1$$ as well, hence my question: why is this function $$f$$ Borel?

• Recall the Feldman--Moore theorem: For any countable Borel equivalence relation $E$, there is a countable group $G$ Borel acting on $X$ such that $E$ is the orbit equivalence relation of $G$. Now quantify over $G$ instead of $X$, and you should get the desired formula complexity. – Edward H Apr 6 at 15:33
• @EdwardH so you mean something like $z\in f^{-1}([x,\infty))\iff \exists y\in X\exists g\in G(y\geq x\land g\cdot y=z)$ which looks like it should be $\mathbf{\Sigma}^1_1$? – TopologicalDynamitard Apr 7 at 20:03
• Something more direct, like $f(x)=y$ iff $(x,y)\in E$ and $\forall g\in G\,(gy\ge y)$. I assume you're also familiar with the fact that if $\{(x,y)\mid f(x)=y\}$ is Borel then $f$ is Borel. – Edward H Apr 8 at 0:35
• @EdwardH I see, very nice! If you write that as an answer I'll be happy to accept it! – TopologicalDynamitard Apr 8 at 9:49

Use Feldman-Moore to fix a countable $$G$$ Borel acting on $$X$$ such that $$E={\sim_G}$$. Now $$f(x)=y$$ iff $$(x,y)\in E$$ and $$\forall g\in G\,(gy\ge y)$$, so $$f$$ is Borel.
• I changed $E=\sim_G$ (coded as E=\sim_G) to $E={\sim_G}$ (coded as E={\sim_G}). This happened because LaTeX, and consequently MathJax, treats \sim in that first example as a part of the binary relation symbol whose first part is the "equals" sign. It's weird how insensitive so many mathematicians are about conspicuous things like this. TeX was designed the way it is because Donald Knuth used his head instead of neglecting things like this. – Michael Hardy Jul 7 at 19:37