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.