二元关系 := 命题函数 or 的子集
时称为 独立无关
元关系类似
[order]
命题函数 是序 :=
- 传递:
- 无环:
也可以用 “等价” 的 版本
- 传递:
- 自反
- 反对称
等价是指
- 如果先有 版本的偏序, 那么定义 之后就有 版本的偏序, 且能变回来 (变回来不是显然的, 需要 偏序的性质来证明, 下同)
- 如果先有 版本的偏序, 那么定义 之后就有 版本的偏序, 且能变回来
Prop 偏序 ==> 非自反 , 即一个量不会 “小于” 它自身. Proof 如果 , 那么无环被破坏
注意: “非自反” (nonreflexive) 不是 not 自反 (not reflexive)
Prop 偏序 ==> () Proof 如果 那么就有 , 矛盾于偏序的非自反
Def
Prop 假设 偏序, 则
Proof
但是偏序 满足 , 所以
所以
Prop 假设 偏序, 则 Proof
但是偏序 满足
Proof <== 显然. 对于 ==>, 假设 . 如果 则由于 , 有 . 如果 那么
于是
Prop (证明不需要 的偏序性质)
- 是自反的
- 是非自反的
Prop 的无环性质 ==> 的反对称性质
Prop 的反对称性质 ==> 的无环性质
Prop 传递 ==> 传递
Prop 传递 + 反对称 ==> 传递
这些命题加起来就证明了 偏序的等价性
Example
-
子集的 “包含” , 或者 “包含且不等于” , 是序
image modified from wiki media about partial order
- 的
- 树图
[order_comparable] comparable := (lt form) or (lte form) :=
[comparable_component] is comparable-component :=
偏序可以分解为相互不 comparable 的 comparable-component. 想象两个毫无关系的树图
[linear_order] 线序
直观上, 线序没有分支, 也称为 “链”
[maximal_linear_order] 极大线序链
let with 线序. is maximal-linear-order := 以下定义等价
它并不能用于分解偏序. 两个极大线序链可以有相交的部分
等价地
- 链无法延拓
链的延拓是指, 存在 且 , 使得, 对每个 , . 延拓后, 也是链
[maximal_linear_order_exists] maximal-linear-order chain alaways exists
也称为 Zorn 引理
需要 选择公理: 如果能够对 (某个类型的) 一些集合证明按照存在某种性质的元素, 那么可以定义一个函数, 将这些集合映射到对应的元素
Proof (ref_29) zorn_lemma.ac in my github repo ac-math ref_30