集合的形式化 #10 基数 (2) 基数的运算

    基数的加法的定义如下：

    其中，sum A B 表示类型 A 和类型 B 的和类型，A 和 B 中的任何一个元素都可不重不漏地对应于 sum A B 中的一个元素。

    “pluscardR”定理为实际处理 card S + card T 的形式提供了一种初步化简的方法。证明该定理时，由于展开定义后直接处理较为复杂，可以先证明“双射集之类型双射”和“eqcardsum”作为铺垫。

    当 card S + card T 中的 S 和 T 类型相同时，可以使用如下定理进一步化简。

    现在可以证明基数的加法具有以下性质：（证明时使用“forall基数2”定理或“forall基数3”定理可将对应于基数的集合控制为类型相同的集合，进而使用上文所述的定理进行化简）

    基数的乘法的定义与性质如下：

    基数的乘方的定义与性质如下：

    以上关于基数运算的定理的证明核心一般是构造双射，而需要构造的双射往往是容易猜出的，故证明的难度不大。

    基数的运算一般可以保持 基数leq 的序，具体定理如下：

    至此，《集合的形式化》完结，更多的关于基数的内容将在自然数的部分展开。敬请期待《实数的形式化》~