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.