Meaning of double colon $::$

Question

I recently came across the following expression regarding function composition:

\begin{equation} g \circ f : A \rightarrow C :: a \mapsto g(f(a)) \end{equation}

I get what this expression is trying to tell me, but I am pretty disturbed by the fact that I don't know what "$::$" means exactly and how to read it. Can anyone tell me what is "$::$"?

Answer 1

In this context it means "defined by", but I've never seen it written like that before. I would have written it "$g \circ f: A \to C$ defined by $a \mapsto g(f(a))$".

Answer 2

I've actually seen this notation with either a single or double colon. Rather compressed notation that really needs you to key into the second arrow being "mapsto" and not just a right arrow. There are a lot of merits to be said for this way of expressing a function, particularly from a lambda calculus / category theory perspective. In addition, just consider the amount of ink and page-space necessary for defining a super messy function on a crazy domain:

Let $$f: \mathbb{R} \to \mathbb{R}$$ be defined by $$f(x) = x^2.$$

versus

Let $f$ be the function $$f: \mathbb{R} \to \mathbb{R} ~~:~~x \mapsto x^2.$$