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

　引理1-3-23 (宇宙的封闭性) 宇宙对秩封闭, 即如果x在某个宇宙里, 那么x的秩也在该宇宙.

设u是宇宙, x ∈ u, 要证ρ x ∈ u. 由ϵ归纳法, 有归纳假设: ∀ y ∈ x, y ∈ u → ρ y ∈ u. 将ρ换成ρ', 由宇宙对并集的封闭性, 即证 [ρ[x]] ∈ u. 由宇宙对替代的封闭性, 只需证以下两个分支.

• ∀ a b,Ρ a = b → a ∈ ρ[x] → b ∈ u. 由函数式替代的定义改写即证对任意y ∈ x有 Ρ (ρ y) ∈ u. 由宇宙对幂集封闭即证ρ y ∈ u, 由归纳假设和宇宙的传递性得证.

∀ a b, ρ a = b → a ∈ x → b ∈ u. 改写即证ρ a ∈ u, 由归纳假设和宇宙的传递性得证 ∎

　Lemma 宇宙对秩封闭 x u : 宇宙 u → x ∈ u → ρ x ∈ u. Proof. intros U xu. induction (正则 x) as [x _ IH]. rewrite ρ等于ρ'. apply 宇宙对并集封闭; auto. repeat apply 宇宙对替代封闭; auto; try congruence. - intros a b <- [y [yx <-]]%函数式替代. apply 宇宙对幂集封闭; auto. apply IH; auto. eapply 宇宙传递; eauto. - intros a b <- ax. apply IH; auto. eapply 宇宙传递; eauto. Qed.

　引理1-3-24 宇宙一定是层.

设u是宇宙, 要证u是层. 只要证u = ⋃ (u ∩ₚ 层), 就可以用层的定义证明u是层. 用外延公理证u = ⋃ (u ∩ₚ 层).

• 要证对任意x ∈ ⋃ (u ∩ₚ 层)有x ∈ u, 即证对x ∈ y ∈ u有x ∈ u, 由宇宙的传递性得证.

• 要证对任意x ∈ u有x ∈ ⋃ (u ∩ₚ 层). 我们证x ∈ Ρ (ρ x) ∈ u ∩ₚ 层.

◦对左边, 由幂集公理和ρ规范得证.

◦对右边, 由分离定理, 要证Ρ (ρ x) ∈ u 且Ρ (ρ x) 是层.

▫对左边, 由宇宙对幂集的封闭性和宇宙对秩的封闭性得证.

▫对右边, 由层的定义和ρ规范得证 ∎

　Lemma 宇宙是层 : 宇宙 ⊑ 层. Proof. intros u U. enough (⋃ (u ∩ₚ 层) = u) as <-. { constructor. now intros x H%分离. } apply 外延. - intros x [y [xy [yu yS]%分离]]%并集. eapply 宇宙传递; eauto. - intros x xu. apply 并集. exists (幂 (ρ x)). split. + apply 幂集, ρ规范. + apply 分离. split. * now apply 宇宙对幂集封闭, 宇宙对秩封闭. * constructor. apply ρ规范. Qed.

　最后, 我们证明本讲的主结论.

定理1-3-25 宇宙等价于对替代封闭的非空极限层.

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