# Defining a set which contains one element per element in another set

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?

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".

This is an application of the Axiom of Choice. One of its formulations (there are several equivalent ones) is that when we have any family of non-empty sets $$A_i, i \in I$$ then there is a so-called choice function $$f: I \to \bigcup_i A_i$$ such that $$f(i) \in A_i$$ for all $$i$$. This AC is what's needed to justify your proof (within set theory):

In your case you have defined $$\mathcal{B}' = \{B \in \mathcal{B}: \exists C \in \mathcal{C}: B \subseteq C\}$$.

Then for each fixed $$B \in \mathcal{B}'$$ we can consider the set $$\mathcal{C}(B):=\{C \in \mathcal{C}: B \subseteq C\}$$ which is a non-empty subset of $$\mathcal{C}$$, by definition, as $$B \in \mathcal{B}'$$ and so we have a choice function $$f: \mathcal{B}' \to \mathcal{C}$$ such that $$f(B) \in \mathcal{C}(B)$$ for all $$B \in \mathcal{B}'$$, so in particular $$B \subseteq f(B) \in \mathcal{C}$$.

In this case we "only" need the countable version of choice (i.e. for countable families) as $$\mathcal{B}'$$ is countable being a subset of $$\mathcal{B}$$, the countable base.

The final step is to note that $$\{f(B): B \in \mathcal{B}'\}$$ is a countable subcover, i.e. the only thing left to check is that it still covers $$X$$.

To this end, let $$x \in X$$. Then there is some $$C_x \in \mathcal{C}$$ that contains $$x$$ and as $$\mathcal{B}$$ is a base and we have an open cover, there is also some $$B_x \in \mathcal{B}$$ with $$x \in B_x \subseteq C_x$$. This shows that $$B_x \in \mathcal{B}'$$ (it has a superset in $$\mathcal{C}$$) and so $$f(B_x)$$ is a set in our subcover, and we know that $$B_x \subseteq f(B_x)$$, so $$f(B_x)$$ also covers $$x$$. As $$x$$ was arbitrary, we are done.