# C-like type declaration.

In most math books declaring an object along with its type is done with the type after a colon after the object, and the definition of this object is done in another expression. E.g.

\begin{align} n & : \mathbb{N} \\ f & :\mathbb{R} \to \mathbb{R}\\ \\ n & := 3. \\ f & := x \mapsto 2x. \end{align}

When I define an object while declaring its type, I do either the following (with the type of the object in the end, after the definiens):

\begin{align} n & := 3 & : \mathbb{N}. \\ f & := x \mapsto 2x & : \mathbb{R} \to \mathbb{R}. \end{align}

Or the following (with the type of the object after the definiendum):

\begin{align} n & : \mathbb{N} & := 3. \\ f &: \mathbb{R} \to \mathbb{R} & := x \mapsto 2x. \end{align}

But is it right to use a notation like in the C programming language, where the type is written before the object with no colon (like in the following example)? Is there a math book which uses this notation instead of the colon one?

\begin{align} \mathbb{N} & \space n := 3. \\ \mathbb{R} \to \mathbb{R} & \space f := x \mapsto 2x. \end{align}

• In "most" math books? I have never seen this in 30+ years. Jan 13 '19 at 14:28
• No, people do not write $n:\Bbb N$ to "declare" $n$. They write $n\in\Bbb N$; which is an assertion to the effect that $n$ is an element of $\Bbb N$. Yes, people do write $f:\Bbb R\to\Bbb R$, but I think it's misleading to think of the colon there as a "declaration" - in fact that line says $f$ is a function from $\Bbb R$ to itself. Jan 13 '19 at 14:41

All four of these are horrible to read. The closest that I've seen to your last is $$f: \mathbb{R}\ni x \mapsto 2x \in \mathbb{R}$$, but that's rare and hiddeous as well. We aren't doing programming: what we're writing is intended to be readable by humans, not parseable by computers. Therefore, you should write something that is easy for humans to read. Sentences are easy for humans to read. For your examples, I'd write "let $$x = 3$$" (no need to specify that it's natural: we can see that) and Define \begin{align*}f:\mathbb{R}\to\mathbb{R}\\:x\mapsto 2x\end{align*}