Mathematical logic and foundations Definition

Function

Builds on Binary relation Uniqueness quantifier

Definition

Let $A$ and $B$ be sets. A function from $A$ to $B$ is a binary relation $f \subseteq A \times B$ such that, for each $a \in A$ , there is exactly one $b \in B$ with $(a, b) \in f$ . This $b$ is the value of $f$ at $a$ , written $f(a)$ . The notation $f \colon A \to B$ says that $f$ is a function from $A$ to $B$ .

Remarks

The set $A$ is the domain and the set $B$ is the codomain of $f$ . Many authors take the triple $(A, B, f)$ as the function. Then two functions with the same pairs but different codomains are different. Two functions $f, g \colon A \to B$ are equal when $f(a) = g(a)$ for each $a \in A$ . Other names are map and mapping.

Where this leads

835 pages build on this one.

Tag	`0XHDTE5YMZ`
URI	`m2://0XHDTE5YMZ`
Kind	definition
Writing	W1 stated
MSC	03E20
Defines	Function
Uses	Binary relation, Uniqueness quantifier

Function

Definition

Remarks

Reading path

Where this leads

Further reading

What this page needs for W2

What links here

Used by