How does $\left\{f\mid f\colon\mathbb{N}\to\mathbb{R}\right\}$ mean 'the set of all real-valued functions of one natural number variable'? On pg. 83 of Hefferon's Linear Algebra, it says this:

The set  $\left \{ f\mid f\colon\mathbb{N}\rightarrow \mathbb{R} \right \}$ of all real-valued functions of one natural number variable is a vector space under the operations.

How do I read the notation to mean what the sentence says? I thought the "|" and ":" mean the same thing--"such that...". So I thought someone would write it $\left \{ f\mid \mathbb{N}\rightarrow \mathbb{R} \right \}$. Also, I don't understand the "$\mathbb{N}\rightarrow \mathbb{R}$" part. I saw from Wikipedia that "$\rightarrow$" means "implies". It makes the notation sound like "$\mathbb{N}$ implies $\mathbb{R}$", which doesn't make sense to me.
 A: $$\begin{array}{ccccc}
\{ & f & | & f & : & \mathbb N & \to & \mathbb R & \} \\
\text{the set of all} & f & \text{such that} & f & \text{is a function from} & \mathbb N & \text{to} & \mathbb R &
\end{array}$$
A: $\to$ in this case means "to." So, $f\colon\mathbb{N}\to\mathbb{R}$ is the notation for a function $f$ with domain $\mathbb{N}$ and codomain $\mathbb{R}$.
$|$ and $:$ both mean "such that" in the context you are suggesting. Here, though, the $:$ is part of the function notation, not the set description notation. So, what you essentially have is s set containing all functions $f$ of the aforementioned form. I.e., a set of all functions which map a natural number to a real number.
A: The notation is slightly sloppy, but not ambiguously so.
In this context, $:$ should be read as "is a function from" and $\to$ should be read as "to".
Then the set is "the set of all objects $f$ such that $f$ is a function from $\mathbb{N}$ to $\mathbb{R}$".
There is no set of all objects $f$, so a priori this set need not exist as an application of the Axiom of Comprehension; this is where the sloppiness comes in.
A: If we read it out loud we would say:
The set of functions $f$ such that the domain of $f$ is $\mathbb N$ and the co-domain of $f$ is $\mathbb R$
