nLab
lambda-abstraction

Idea

$\lambda$-Abstraction is the process of interpreting a formula for a function (or operation) as defining an actual function.

Notation

If in a context with a free variable $x$ of type $A$ we have a term $t$ of type $B$, then

(1)$${\lambda }_{x:A}t$$\lambda_{x\colon A} t

is a term (in a context without the free variable) of the dependent product type ${\prod }_{x:A}B$. If $B$ is defined in the context without the free variable, then this expression is a term of the function type $A\to B$ or $B^A$.

Often we make the presence of the free variable explicit in the notation, saying that $t[x]$ is a term of type $B[x]$; then

(2)$${\lambda }_{x:A}t[x],$$\lambda_{x\colon A} t[x] ,

a term of the dependent product ${\prod }_{x:A}B[x]$. Or if $t[x]$ is a term of the constant type $B$, then the same expression is a term of the function type $A\to B$.

In set theory

Although developed for type theory and commonly used in computer science, $\lambda$-abstraction makes sense in ordinary mathematics usually based on set theory. If the types $A$ and $B$ are interpreted as sets and we define functions as certain subsets of cartesian products, then the notation (2) refers to

$$\{(x,y)\in A\times B\mid y=t[x]\}$$\{ (x,y) \in A \times B \;|\; y = t[x] \}

(at least in the simple case where $B$ is constant).