# OpenMath Content Dictionary: fns3

Canonical URL:
http://www.openmath.org/cd/fns3.ocd
CD Base:
http://www.openmath.org/cd
CD File:
fns3.ocd
CD as XML Encoded OpenMath:
fns3.omcd
Defines:
function, specification
Date:
2004-06-01
Version:
1 (Revision 1)
Review Date:
2006-06-01
Status:
experimental

This CD holds further functions concerning functions themselves. A particularly interesting function is

function

which constructs a function with given domain and range.

## function

Description:

This symbol denotes a function constructor. When aplied to at least two arguments, which are sets, the first argument is the domain and the second the range of the function. When applied to at least three arguments, the first two of which are stes and the third of which is a lambda expression, the third argument gives the function specification.

Commented Mathematical property (CMP):
The domain of the function f constructed this way is the first argument
Formal Mathematical property (FMP):
$\mathrm{domain}\left(\mathrm{function}\left(X,Y,Z\right)\right)=X$
Commented Mathematical property (CMP):
The range of the function f constructed this way is the second argument
Formal Mathematical property (FMP):
$\mathrm{range}\left(\mathrm{function}\left(X,Y,Z\right)\right)=Y$
Example:
The following object defines a function from the natural numbers into the integers specificied by the fact that n maps to n(n+1)/2.
$\mathrm{function}\left(\mathbb{N},\mathbb{Z},\lambda n.\frac{n\left(n+1\right)}{2}\right)$
Signatures:
sts

 [Next: specification] [Last: specification] [Top]

## specification

Description:

This symbol denotes the specification of a function. It is a unary function. When aplied to its argument, which should be a function applied to three arguments, it returns the third argument of the function, that is, the function specification.

Formal Mathematical property (FMP):
$\mathrm{specification}\left(\mathrm{function}\left(\mathbb{N},\mathbb{Z},f\right)\right)=f$
Example:
The following object defines a function from the natural numbers into the integers specificied by the fact that n maps to n(n+1)/2.
$\mathrm{specification}\left(\mathrm{function}\left(\mathbb{N},\mathbb{Z},\lambda n.\frac{n\left(n+1\right)}{2}\right)\right)=\lambda n.\frac{n\left(n+1\right)}{2}$
Signatures:
sts

 [First: function] [Previous: function] [Top]