[Math] Does the colon in function notation stand for “such that”

notation

The colon mark sometimes stands for "such that".

When writing functions, it is customary to write, for example:

$f:[0,1]\rightarrow[0,1]$.

Can the colon in this context be interpreted as "such that"?

If not, is it just a historical quirk that ":" is used in this context, but sometimes also means "such that"?

Best Answer

In type theory the same notation is used, where f:x->y means that f is of the function type x->y, which in set-theoretical terms means that f is an element of the function set x^y. Type theorists would for instance also write z:x×y to say that z of of the product type, i.e. that z is an element of the set x×y in set theory.

Though I'm not sure if the type theorists copied the notation from the mathematicians or the other way around.

Related Question