数学知识
• SF第1卷
• 集合模型论(1-1): 从封闭类构造内模型
• 集合模型论(1-2): 累积层级与集合的秩
• 最好了解后继序数与极限序数, 否则就跳过文章中提及序数的内容, 不影响主线.
极限层
上一篇我们讲了怎么在不引入序数的前提下定义累积层级和集合的秩. 接下来将展示, 即使没有后继序数与极限序数, 我们也可以研究后继层与极限层.
定义1-3-1 (后继层) 我们说x是后继层, 当且仅当存在层y使得 x =Ρ y.
定义1-3-2 (极限层) 我们说x是极限层, 当且仅当x是层且 x ⊆ ⋃ x.
Definition 后继层 x := ∃ y ∈ₚ 层, x = 幂 y. Definition 极限层 x := x ∈ₚ 层 ∧ x ⊆ ⋃ x.
不难看出, 它们跟后继序数和极限序数的定义有类似的形式. 只是按极限序数的定义, 我们应该有 x = ⋃ x. 这可以证明.
备注1-3-3 x是极限层, 当且仅当x是层且 x = ⋃ x.
按极限层的定义右到左是显然的. 左到右用外延公理证x = ⋃ x,按极限层的定义只需证⋃ x ⊆ x, 由层的传递性得证 ∎
Remark 极限层等价定义 x : 极限层 x ↔ x ∈ₚ 层 ∧ x = ⋃ x. Proof. split. - intros [xS sub]. split. auto. apply 外延. auto. apply 并得子集. firstorder using 层传递. - intros [xS eq]. split. auto. rewrite eq at 1. zf. Qed.
另外需要注意按此定义, 空集也是极限层, 所以后文中如有必要会用"非空极限层"以明确所指.
引理1-3-4 如果x是层之集(由层组成的集合), 那么要么⋃ x ∈ x要么x ⊆ ⋃ x.
假设x ⊈ ⋃ x, 则存在y ∈ x且y ∉ ⋃ x. 我们证⋃ x就是y. 只需证y是x的上界, 即对任意z ∈ x有z ⊆ y. 由于y是层, 由层的ϵ线序, 若z ⊈ y, 只能有y ∈ z, 这会导致y ∈ ⋃ x与前提矛盾 ∎
Lemma 层之集二分 x : x ⊆ₚ 层 → ⋃ x ∈ x ∨ x ⊆ ⋃ x. Proof. intros sub. 排中 (x ⊆ ⋃ x); auto. left. apply 非子集 in H as [y[yx yns]]. replace (⋃ x) with y; auto. symmetry. apply 并即上确界. split; auto. intros z zx. destruct (层线序 (sub z zx) (sub y yx)); auto. exfalso. apply yns. apply 并集. now exists z. Qed.
事实1-3-5 层要么是后继层要么是极限层.
设x是层, 对层x归纳, 要证两种情况.
要证当x是层时, 对Ρ x命题成立. 按定义 Ρ x是后继层.
要证当x是层之集时, 对⋃ x命题成立. 另外我们有归纳假设: 对任意y ∈ x命题成立. 对x用引理1-3-4, 分两种情况.
若⋃ x ∈ x, 由归纳假设立即得证.
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。