TeXipedia

coloncolonequals

Represents a definition or declaration relationship, commonly used in mathematical and computer science notation to indicate that something is being defined.

Overview

Serves as a specialized definition symbol that combines colons and equals to create a visually distinct operator for formal definitions and declarations.

  • Popular in formal mathematics and theoretical computer science for defining functions, sets, or types
  • Provides clearer visual distinction than a simple equals sign when introducing new mathematical objects
  • Often used in programming language semantics and type theory
  • Helps readers quickly identify definition statements in complex mathematical texts

Examples

Defining a function in type theory or formal mathematics.

f∷=λx.x2f \coloncolonequals \lambda x. x^2 
f \coloncolonequals \lambda x. x^2

Specifying a type definition in mathematical logic.

N∷={0,1,2,…}\mathbb{N} \coloncolonequals \{0,1,2,\ldots\} 
\mathbb{N} \coloncolonequals \{0,1,2,\ldots\}

Declaring a formal mathematical sequence definition.

an∷=1n2a_n \coloncolonequals \frac{1}{n^2} 
a_n \coloncolonequals \frac{1}{n^2}