集合的形式化 #6 函数 (2)

    在上一篇专栏中我们研究了函数的基本属性，现在我们可以开始研究一些具体的函数和函数的运算。我们从空函数开始：A 类型到 B 类型的空函数为 fun _ : A => @None B，它的性质如下：

    分段函数的定义与性质：

    f_DL S f 表示将函数 f 的定义域限制在 S 的范围内后所得的函数，它的定义与性质如下：

    常数函数的定义与性质：

    f_id S 表示定义域为 S 且定义域中的每个元素的函数值均为其本身的函数，它的定义与性质如下：

    反函数的定义与性质：

    复合函数的定义与性质：