补丁（3）论文集合模型论部分篇。 (6-2)

若x ⊆ ⋃ x, 我们证⋃ x是极限层. 首先由 x是层之集 和 层的定义, ⋃ x是层. 还需证 ⋃ x ⊆ ⋃ ⋃ x, 即证对任意y ∈ ⋃ x (即对任意满足 y ∈ z ∈ x的y和z) 有y ∈ ⋃ ⋃ x. z就见证了y ∈ z ∈ ⋃ x, 其中后半部分由x ⊆ ⋃ x和z ∈ x得证 ∎

Fact 层二分 x : x ∈ₚ 层 → x ∈ₚ 后继层 ∨ x ∈ₚ 极限层. Proof. induction 1 as [x xS _|x xS IH]. - left. exists x. auto. - destruct (层之集二分 xS). + apply IH, H. + right. split. now constructor. intros y [z [yz zx]]%并集. apply 并集. exists z. auto. Qed.

　封闭性

我们来考察极限层的封闭性. 由于层是集合而不是类, 我们仿照1-1封闭类的定义, 定义封闭集.

定义1-3-6 (封闭集) 如代码.

Definition 空集封闭 x := ∅ ∈ x. Definition 并集封闭 x := ∀ y ∈ x, ⋃ y ∈ x. Definition 幂集封闭 x := ∀ y ∈ x, 幂 y ∈ x. Definition 替代封闭 x := ∀ R y, 函数性 R → (∀ a b, R a b → a ∈ y → b ∈ x) → y ∈ x → R @ y ∈ x. Definition 替代封闭' x := ∀ R y, 函数性 R → R @ y ⊆ x → y ∈ x → R @ y ∈ x. Definition 配对封闭 x := ∀ a b ∈ x, {a, b} ∈ x. Definition 分离封闭 x := ∀ P, ∀ y ∈ x, y ∩ₚ P ∈ x.

事实1-3-7 定义1-3-6中对替代的两种封闭性定义是等价.

见Github仓库 ∎

Fact 替代封闭_等价表述 x : 替代封闭 x ↔ 替代封闭' x.

对替代的封闭性我们只采用第一种定义.

我们先给出结论: 对极限层来说, 除了对替代的封闭性不成立, 定义1-3-6中的其他5种都成立. 为了使证明更可读, 我们补充3个引理.

引理1-3-8 对集合取并不改变其秩, 即对任意x ∈ 层y, ⋃ x ∈ 层y.

对层y归纳.

要证x ∈ Ρ y 蕴含 ⋃ x ∈ Ρ y, 即证对任意a ∈ b ∈ x ⊆ y有a ∈ y, 由层的传递性得证.

要证对层之集y, x ∈ ⋃ y (即x ∈ a ∈ y) 蕴含 ⋃ x ∈ ⋃ y. 我们证前件的a就见证了⋃ x ∈ a ∈ y, 只需证⋃ x ∈ a. 这由归纳假设: 对任意z, x ∈ z ∈ y蕴含⋃ x ∈ z 得证 ∎

Lemma 并_等秩 x y : x ∈ y → y ∈ₚ 层 → ⋃ x ∈ y. Proof. intros xy. induction 1 as [y yS _|y yS IH]. - apply 幂集 in xy. apply 幂集. intros a [b [ab bx%xy]]%并集. eapply 层传递; eauto. - apply 并集 in xy as [a [xa ax]]. apply 并集. exists a. split; auto. Qed.

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。