In mathematics, the notation $~$f : X \to Y$~$ (here, "colon-to notation," because the arrow $~$\to$~$ is written "\to" in LaTeX) means that $~$f$~$ is a function with domain $~$X$~$ and codomain $~$Y$~$. It can be read "$~$f$~$, a function from $~$X$~$ to $~$Y$~$."

This can be thought of as ascribing a function type to the value $~$f$~$. The use of a colon to express that a given value has a given type, as is done in type theory, is a generalization of this notation.

Examples

$~$f : \mathbb{R} \to \mathbb{R}$~$ means that $~$f$~$ is a function from the real numbers to the real numbers, such as $~$x \mapsto x^2$~$ (mapsto notation).

$~$f : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$~$ means that $~$f$~$ is a function from pairs of real numbers to real numbers. The $~$\times$~$ here refers to the Cartesian product of sets.