Uniformization of a binary relation (source code)

= Uniformization of a binary relation

For $A\subseteq X\times Y$, a uniformization is a <function> $f$ on the projection of $A$ to $X$ such that $(x,f(x))\in A$ for every $x$ in that projection. It chooses one witness from every nonempty vertical section of $A$.