I'm doing a bunch of topology exercises at the moment, and one thing I sometimes want to express is "given set $X$, let $Y$ be a set which contains an element per element in $X$". As an example, here's an attempted proof that second-countable spaces are Lindelöf:
Let $X$ be a second-countable topological space. Let $\mathcal B$ be some countable basis for its topology. Let $\mathcal C$ be an open cover of $X$. Let $\mathcal B'=\{B\in \mathcal B:\exists C\in \mathcal C\text{ such that }B\subseteq C\}$.
Let $\mathcal C'$ be a subcover of $\mathcal C$ which for each $B\in \mathcal B'$ contains one $C\in \mathcal C$ such that $B\subseteq C$.
What bothers me is the last line. It feels like it could have been more readable with set builder notation, but how do I express it?
How about this:
Let $\alpha:\mathcal B'\to\mathcal C$ be a function sending each $B\in\mathcal B'$ to some $C\in\mathcal C$ sthat satisfies $B\subseteq C$.
Now let $\mathcal C'$ be the image of $\alpha$, i.e. $\mathcal C'=\{\alpha(B)\mid B\in\mathcal B'\}$.
Actually $\alpha$ is a "choice function".