函数

形式陈述 ​

总函数可视为部分函数公理库部分函数Partial function只在定义域某个子集上赋值、允许部分输入无输出的函数。的特例：部分函数只要求在定义域的某个子集上至多给出一个输出，总函数再要求每个输入都落在实际定义域内。

本库采用函数由定义域、陪域和映射规则共同组成的约定。为把这些数据编码进对象本身，将函数定义为三元组

$$f=(A,B,{\mathrm{\Gamma }}_f),$$

其中 $A$ 是定义域，$B$ 是陪域，${\mathrm{\Gamma }}_f\subseteq A\times B$ 是一个关系公理库关系Relation · Binary relation带源集与目标集的二元关系，其底层关系图是 A×B 的子集。，称为函数图，并满足

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

这个唯一的 $b$ 记为 $f(a)$，并写作 $f:A\to B$。像集为

$$f[A]=\{f(a):a\in A\}\subseteq B.$$

函数相等约定 ​

按本库约定，两个函数相等，当且仅当它们的定义域、陪域和函数图都分别相等。部分文献采用另一约定，只比较函数图或定义域与取值规则，并把陪域当作外部类型信息；两种写法都可使用，但讨论函数相等、满射和复合时必须先固定约定。除非条目显式另作声明，本库所有函数、映射、同态与算子页面都沿用这里的带陪域相等约定。

像、逆像与复合 ​

对 $S\subseteq A$，像定义为

$$f[S]=\{f(a):a\in S\}\subseteq B.$$

对 $T\subseteq B$，逆像定义为

$$f^{-1}[T]=\{a\in A:f(a)\in T\}.$$

逆像不要求 $f$ 可逆；上标 $-1$ 在这里表示集合运算，而不是反函数。逆像保持并、交和相对补：

$$f^{-1}\left[\bigcup _i{T}_i\right]=\bigcup _i{f}^{-1}[T_i],f^{-1}[B\setminus T]=A\setminus f^{-1}[T].$$

像保持并，却一般不保持交或补，因为不同输入可能合并到同一输出。这个不对称是可测函数、连续函数和同态中许多“结构由逆像拉回”定义的共同原因。

若 $f:A\to B$、$g:B\to C$，复合公理库函数复合Function composition · Composition of maps按先 f 后 g 的次序把映射串联为 g∘f。 $g\circ f:A\to C$ 定义为 $(g\circ f)(a)=g(f(a))$。陪域与定义域的类型必须接合；只知道两个公式能代入，不足以忽略它们声明的类型。复合满足结合律，恒等函数是单位元。

直觉

函数是一条带类型的输入—输出规则。“每个输入”要求定义域中的点不能遗漏，“唯一输出”排除一对多；不同输入仍可共享同一输出，所以函数不必是单射。公式、算法和查表只是描述 ${\mathrm{\Gamma }}_f$ 的不同方式，既不自动给出允许哪些输入，也不自动给出结果被视为落在哪个集合。正因陪域属于数据，同一公式在不同陪域下可以有不同的满射性。

例子与边界

平方函数

$$f:\mathbb{R}\to \mathbb{R},x\mapsto x^2,g:\mathbb{R}\to [0,\mathrm{\infty }),x\mapsto x^2$$

拥有相同的定义域和函数图，却有不同陪域，因此是不同函数；$g$ 满射而 $f$ 不是。关系 $x^2+y^2=1$ 若把 $x$ 当输入、$y$ 当输出，通常同时允许正负两个 $y$，所以不是函数。类似地，$y^2=x$ 只有在额外选择非负平方根后才给出从 $[0,\mathrm{\infty })$ 到 $[0,\mathrm{\infty })$ 的函数。

当定义域为空时，${\mathrm{\Gamma }}_f=\varnothing$ 对任意陪域 $B$ 都满足条件，因而存在唯一函数 $\varnothing \to B$。若定义域非空而陪域为空，则不存在函数，因为任何输入都找不到输出。

推论与应用

单射、满射与反函数 ​

单射公理库单射Injective function · One-to-one function不同输入必有不同输出的函数。约束不同输入是否合并，满射公理库满射Surjective function · Onto function陪域中每个元素都有至少一个原像的函数。要求像集覆盖陪域，双射同时满足二者。只有双射才存在两侧反函数 $f^{-1}:B\to A$，满足

$$f^{-1}\circ f={\mathrm{id}}_A,f\circ f^{-1}={\mathrm{id}}_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。