形式陈述

函数 $f:A\to B$ 是关系 $f\subseteq A\times B$，满足

$$\mathrm{\forall }a\in A\mathrm{\exists }!b\in B((a,b)\in f).$$

$A$ 是定义域，$B$ 是陪域，唯一的 $b$ 记为 $f(a)$；像集为 $f[A]=\{f(a):a\in A\}\subseteq B$。

直觉

函数要求每个合法输入恰有一个输出。公式、算法或查表只是描述函数的方式；陪域属于函数类型的一部分。

例子与边界

$f:\mathbb{R}\to \mathbb{R},f(x)=x^2$ 是函数。关系 $x^2+y^2=1$ 若把 $x$ 作为输入、$y$ 作为输出，则通常一对多，不是函数。空定义域到任意 $B$ 存在唯一空函数；非空定义域到空陪域不存在函数。

推论与应用

函数是算法规格、随机变量、同态和坐标变换的共同抽象。单射、满射、双射与复合描述函数保留和覆盖信息的方式。

参考资料

• Paul R. Halmos, Naive Set Theory, 1960; Dover reprint 2017, §§8–10。
• Daniel J. Velleman, How to Prove It: A Structured Approach, 3rd ed., Cambridge University Press, 2019, Functions chapter。