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

引理1-3-9 对集合取幂将提升其秩, 即对任意x ∈ 层y,Ρ x ∈ 层Ρ y.

对层y分类讨论.

• 若x ∈ Ρ y, 要证 x ∈ Ρ y, 即证x ⊆ ΡΡ y 蕴含Ρ x ⊆ Ρ y, 显然成立.

• 若y是层之集且有x ∈ ⋃ y (即x ∈ a ∈ y), 要证Ρ x ∈ Ρ ⋃ y, 即证对任意b ⊆ x有b ∈ ⋃ y. 我们证b ∈ a ∈ y, 只需证b ∈ a, 由层的膨胀性得证 ∎

　Lemma 幂_升秩 x y : x ∈ y → y ∈ₚ 层 → 幂 x ∈ 幂 y. Proof. intros xy. destruct 1 as [y _|y yS]. - apply 幂集 in xy. apply 幂集. now apply 幂单调. - apply 并集 in xy as [a [xa ay]]. apply 幂集. intros b bx%幂集. apply 并集. exists a. split; auto. eapply 层膨胀; eauto. Qed.

定义1-3-10 (秩封闭) 我们说x对秩封闭, 当且仅当对x中的任意集合y, 存在一个层z容纳y, 且z也在x中.

Definition 秩封闭 x := ∀ y ∈ x, ∃ z ∈ₚ 层, y ∈ z ∧ z ∈ x.

引理1-3-11 极限层对秩封闭.

设x是极限层, 对层x归纳, 要证两种情况.

• 要证Ρ x ⊆ ⋃ Ρ x = x 蕴含Ρ x对秩封闭, 前提有矛盾.

• 要证 ⋃ x ⊆ ⋃ ⋃ x 蕴含 ⋃ x对秩封闭. 另外我们有归纳假设: x的任意成员y满足 ⋃ y ⊆ ⋃ ⋃ y 蕴含 ⋃ y对秩封闭. 由引理1-3-4, 分两种情况.

◦若⋃ x ∈ x, 使用归纳假设得证.

◦若x ⊆ ⋃ x, 要证对y ∈ ⋃ x存在层z满足y ∈ z ∈ x, 显然成立 ∎

Lemma 极限层对秩封闭 : 极限层 ⊑ 秩封闭. Proof. intros x [xS sub]. induction xS as [x _ _|x xS IH]. - rewrite 并幂 in sub. now apply 幂集在上 in sub. - destruct (层之集二分 xS). now apply IH. intros y [z [yz zx]]%并集. exists z. auto. Qed.

回到封闭性的证明.

引理1-3-12 非空层对空集封闭.

设非空层x. 由于空集也是层, 由层的ϵ线序, 要么 x ⊆ ∅, 这意味着x为空集, 与前提矛盾; 要么 ∅ ∈ x, 命题得证 ∎

Lemma 非空层对空集封闭 x : x ∈ₚ 层 → 非空 x → 空集封闭 x. Proof. intros xS [y yx]. destruct (层线序 xS 空集层); auto. apply H in yx. zf. Qed.

引理1-3-13 极限层对并集封闭.

引理1-3-8已证任意层对并集封闭, 极限这个条件是多余的 ∎

Lemma 极限层对并集封闭 : 极限层 ⊑ 并集封闭. Proof. intros x [xS _] y yx. now apply 并_等秩. Qed.

　引理1-3-14 极限层对幂集封闭.

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