note-math

自然数 的加法

Proof 在现实世界的直观是, 对于数数 , 无论怎样把数数任务手动分成几个子任务, 都不会影响结果, 而且总的分解方式有限, 最终的分解是大量 的交换律和结合律

自然数 的乘法

整数

有理数

实数

无理数的例子

代数数

注意不要求 , 不限制 , 包含所有有理数 , 部分无理数 e.g.

代数数 是可数集, 实数 是不可数集

超越数 . 是超越数

十进制, 二进制都可以定义实数, 都是特殊的区间套方法

有理数区间是子集 with property 序不中断

注意区间端点可以不是有理数. 用区间套定义实数还需要处理 Cauchy 性质或者叫做 limit-distance-vanish 性质

从操作简单性来说, 应该用 Dedekind-cut. “操作简单” 是指

• let , 一一对应
• 所以 和 一一对应

[Dedekind_cut] 无理数

实数

逻辑上等价地可以只使用一半, 例如, 有理数 的任何左半无限区间, 然后自动通过做 中的补集得到右半无限区间. 但这里用更对称的表示

• [order_real] 序

let

• [add_real] 加法. let

由于 的存在, 乘法不保持序. 但是 的乘法保持序. 先处理 的情况, 再用反射 得到 的情况

• [multiply_real] 乘法. let

的 都有结合律, 交换律, 分配律

[completeness_real] 完备性

[exact_bound] 确界原理

[nested_closed_interval_theorem] 闭区间套定理

[closed_interval_intersection_theorem]

[closed_interval_net_theorem] 闭区间 网 交集非空

Proof

反方向 “闭区间族的小端点都 大端点 ==> 区间网” 不成立, 考虑只有两个区间 且交集非空 且 的闭区间族, 没有第三个区间属于它们的交集. 虽然只要补充交集, 就能满足

let

def 序列 单调递减, 单调递增

[limsup] 上极限

[liminf] 下极限

Example

对于 序列定义

对于一般 net 定义

[limit_distance_vanish_sequence] := . i.e. tail distance vanish

[limit_distance_vanish_net] :=

[Cauchy_completeness_real] limit-distance-vanish 序列 or net 收敛

Proof

反过来, 收敛序列是 limit-distance-vanish 的. by 三角不等式

Prop 序列 or net 收敛到 <==> limit-distance-vanish

[uncountable_real] 实数不可数