What does this notation mean: $F_n:\aleph_0\to\{0,1\}:k\mapsto F(x_n,k)$

Question

This is a line from this answer by Brian Scott (unfortunately no longer active here). Forcing Question about a sequence of functions from $\aleph_{0}$ into $2 = \{0, 1\}$

I have a sense as to how the separate pieces work, but don't know how thing work in total.

$$F_n:\aleph_0\to\{0,1\}:k\mapsto F(x_n,k)\;$$

Thanks

Answer 1

Read in English: $$\mbox{"$F_n$ is the map from $\aleph_0$ to $\{0, 1\}$ which sends $k$ to $F(x_n, k)$."}$$ One important aspect is the difference between "$\rightarrow$," which is used to describe domain/range, and "$\mapsto$" (whose latex code is "\mapsto"), which describes the value of the function on a given input.

So for example, we could describe the function on the naturals which sends everything to $0$ as $$c: \mathbb{N}\rightarrow\mathbb{N}: n\mapsto 0.$$

---

Another less trivial example to help:

Consider Cantor's diagonal argument to prove that the set of functions from $\mathbb{N}$ to $\mathbb{N}$ is uncountable.

In natural language, this can be phrased as: "Given a list $(f_i)_{i\in\mathbb{N}}$ of maps $\mathbb{N}\rightarrow\mathbb{N}$, we let $g$ be defined by $g(i)=f_i(i)+1$; then [rest of argument]."

Using the notation above, we can write this instead as: "Suppose $F:\mathbb{N}\rightarrow\mathbb{N}^\mathbb{N}$. ($F$ is just a sequence of functions from naturals to naturals - "$\mathbb{N}^\mathbb{N}$" is the set of functions from naturals to naturals, and a function $h: \mathbb{N}\rightarrow A$ can be thought of as a sequence of elements of $A$ whose $n$th term is $h(n)$.) We let $g$ be $$g:\mathbb{N}\rightarrow\mathbb{N}: i\mapsto f_i(i)+1.$$ Then [rest of argument]."

---

Depending on your background, the "$\mapsto$" idea may be made more simple if you think in terms of $\lambda$ notation: if we say "$j: A\rightarrow B: a\mapsto [thing]$," we're describing the object "$\lambda x^A. [thing]$." (I'm writing "$x^A$" to denote that $x$ is a variable of type $A$, and I'm being rude and conflating sets and types a bit, but hopefully the point is clear-ish; if not, ignore this part.)

Answer 2

Usually it is written as

\begin{align} F_n &:\aleph_0\to\{0,1\} \\ &:k \mapsto F(x_n,k) \end{align}

and it describes a function $F_n :\aleph_0\to\{0,1\}$ defined by $F_n(k)=F(x_n,k)$ where, $k \in \aleph_0$ and $F$ is something like $F:\mathbf S^{\mathbb N} \times \aleph_0 \to \{0,1\}$ for some set $\mathbf S$.