米泽对 Walter Rudin 的《数学分析原理》/基础拓扑的评论

有限集、可数集和不可数集

如前所述，这本书没有正确地介绍关系。在 Mizar 中，函数是一种特殊的关系(参见RELAT_1:def 1)，因此，关于函数的许多看似显而易见的结论对于关系来说更为普遍，因此它们在RELAT_1而不是FUNCT_1.

2.1 定义
一个函数 $f$ 由以下定义FUNCT_1:def 1. $f(x)$ 是f.x (FUNCT_1:def 2). 一个A,B 的函数在FUNCT_2中定义，它的主要属性由FUNCT_2:def 1, RELAT_1:def 18和RELAT_1:def 19编码。$f$ 的定义域/值域dom f/rng f最初在XTUPLE_0:def 12/13中定义，并在RELAT_1. rng f中重新命名，在FUNCT_1:def 3.

2.2 定义
$f(E)$ 是f.:E (RELAT_1:def 13, FUNCT_1:def 6)，该备注是RELAT_1:113. $f(A)\subset B$ 在RELSET_1中编码。满射是onto (FUNCT_2:def 3).
$f^{-1}(E)$ 是f"E (RELAT_1:def 14, FUNCT_1:def 7). $f^{-1}(y)$ 是f"{y}或Coim(f,y) (RELAT_1:def 17). 书中没有关于“一对一”的第一个定义的参考，但第二个定义是FUNCT_1:def 4.

2.3 定义
$A$ 和 $B$ 的一一对应关系由以下表示A,B are_equipotent (WELLORD2)，这等同于它们的基数是CARD_1:5. 反身性和对称性在WELLORD2:def 4中编码，传递性是WELLORD2:15. 另一方面，基数的反身性、对称性和传递性是通过=谓词内置的。
一个关系是反身, 对称和传递的性质由RELAT_2:def 9, RELAT_2:def 11和RELAT_2:def 16分别给出。等价关系在EQREL_1. 在 Mizar 中，一个关系是一个适当的集合，由于一个反身关系包含自身的副本，因此在 Mizar 中无法用关系表示集合的一一对应关系，因为没有集合的集合。

2.4 定义
$J_{n}$ 是Seg n (FINSEQ_1:def 1)，$J$ 是NATPLUS (NAT_LAT:def 6)，尽管应该提到在 Mizar 中NAT (ORDINAL1:def 11，在NUMBERS中引入的同义词）是 $J\cup \{0\}$ 更常用。非负整数通常用let n be Nat，正整数用let n be non zero Nat (ORDINAL1:def 14) 而不是let n be Element of NATPLUS. 因此，可数性用NAT.
(a) 定义等同于 Mizar 中的定义（FINSET_1:def 1）。如果X 是有限的，则 $X$ 是有限的，根据FINSEQ_1:56。如果 $X$ 是有限的，则card X = card Seg n = n根据（FINSEQ_1:57），则card X 是有限的 (自然数 -> 有限聚类在CARD_1），因此X 是有限的（因为对于无限的 $X$card X -> 无限聚类在CARD_1).
(b) 给出为有限在FINSET_1.
中的反义词可数的 (CARD_3:def 15).
(d) 给出为可数的在CARD_3.
中的反义词可数的 (CARD_3:def 14).

2.5 例子 聚类在GAUSSINT.

2.6 备注 没有参考。#TODO 找到X 是无限的当且仅当存在 Y 为 X 的真子集，使得 X，Y 等势

2.7 定义
具有特定定义域 $X$ （但不一定有特定值域）的函数，一个X 的多排序集是一个X 上的总定义函数 (PBOOLE）。则 Mizar 中的序列（从 $0$ 而不是 $1$ 开始）是一个NAT 的多排序集。如果它是一些 $A$ 的元素的序列，则它也可以被描述为一个A 的序列 (NAT_1).
之后给出的备注部分编码在DICKSON:3中，但没有参考。

2.8 定理 没有参考。#TODO 找到令 X 为可数集；聚类无限 -> 可数用于 X 的子集

2.9 定义
索引集族是一个多排序集，如上所述。如果仅给出一个 $E$ 的子集集合 $\Omega$，那将是一个子集族 (SETFAM_1）。由于任何对象在 Mizar 中都是一个集合，所以函子union E (TARSKI:def 4）无需该概念。 $E_{1}\cup E_{2}$ 是E1 \/ E2 (XBOOLE_0:def 3）。$E$ 的交集是meet E (SETFAM_1:def 1）。$E_{1}\cap E_{2}$ 是E1 /\ E2 (XBOOLE_0:def 4）。$A$ 和 $B$ 的交集是A meets B（作为下一个谓词在XBOOLE_0中的反义词），否则A misses B (XBOOLE_0:def 7).

2.10 例子
(a) 没有参考。
(b) 没有参考。

2.11 备注
(8) 在定义中接线XBOOLE_0:def 3/4.
(9) 是XBOOLE_1:4和XBOOLE_1:16.
(10) 是XBOOLE_1:23（另一个是XBOOLE_1:24).
(11) 是XBOOLE_1:7.
(12) 是XBOOLE_1:17.
（13）已内置，具有正确的要求。
(14) 是XBOOLE_1:12和XBOOLE_1:28.

2.12 定理 没有参考。#TODO 找到集族并集是可数的，如果它中的每个集合最多是可数的，并且至少有一个是可数的

推论 是CARD_4:12.

2.13 定理 是CARD_4:10.

推论 是TOPGEN_3:17.

2.14 定理
TOPGEN_3:29与CARD_2:def 3和CARD_1:50组合表明 0-1 序列的基数与REAL. TOPGEN_3:30的基数相同，表明实数不可数。

度量空间

2.15 定义 是MetrSpace (METRIC_1），通过METRIC_1:def 6-9（分别指的是METRIC_1:def 2-5）。

2.16 例子
如前所述，$R^{k}$ 作为度量空间是Euclid n (EUCLID:def 7），$R^{1}$ 也是 RealSpace（METRIC_1:def 13).
$Y$ 的子集作为度量空间是通过Y 的子空间 (TOPMETR:def 1）和TOPMETR:def 2.
TODO 参考最后两个例子。

2.17 定义
$(a,b)$ 是].a,b.[ (XXREAL_1:def 4），$[a,b]$ 是[.a,b.] (XXREAL_1:def 1），$[a,b)$ 是[.a,b.[ (XXREAL_1:def 2），$(a,b]$ 是].a,b.] (XXREAL_1:def 3).
一个$k$-胞是cell(a,b) (CHAIN_1:def 6).
中心为 $x$，半径为 $r$ 的开/闭球由Ball(x,r)/cl_Ball(x,r) (METRIC_1:def 14/15给出，度量空间为TOPREAL9:def 1/2对于TOP-REAL k).
凸集由CONVEX1:def 2（用于TOP-REAL k，但不用于Euclid k）。开/闭球在TOPREAL9中被聚集为凸。对于凸性胞没有参考。 TODO 找到它。

2.18 定义
（a）是Ball(p,r) (METRIC_1:def 14)
(b) 没有参考。
（c）没有参考。
（d）没有参考。
（e）没有参考。
（f）没有参考。
（g）没有参考。
（h）没有参考。
（i）是TBSP_1:def 7或METRIC_6:def 3.
（j）没有参考。

2.18 定义（对于拓扑空间和TOP-REAL k)
拓扑空间的基本知识在PRE_TOPC.
（a）是Ball(p,r) (TOPREAL9:def 1)
（b）"$p$ 是 $E$ 的极限点" 基本上是p 是 E 的聚点 (TOPGEN_1:def 2），这用TOPS_1:12来表示。$E$ 的所有极限点集，即 $E$ 的导数是Der E (TOPGEN_1:def 3），它通过TOPGEN_1:17.
给出了第二个特征。（c）就像这样，“$p$ 是 $E$ 的孤立点”是p 是 E 中的孤立点 (TOPGEN_1:def 4).
（d）是TOPGEN_4:3。一个集合被定义为闭的在PRE_TOPC:def 3.
中的反义词TOPS_1:22。$E$ 的内部是Int E (TOPS_1:def 1).
（f）是TOPS_1:23。一个集合被定义为开的在PRE_TOPC:def 2.
（g）是SUBSET_1:def 4，另请参见XBOOLE_0:def 5.
（h）是TOPGEN_1:def 10与TOPGEN_1:def 7。另请参见TOPS_1:5和TOPGEN_1:28。（i）没有参考。
（j）由TOPS_1:def 3和TOPGEN_1:29.

2.19 定理 没有参考。

2.19 定理（对于拓扑空间和 TOP-REAL n）TOP-REAL k在TOPREAL9.

2.20 定理 无参考。

2.20 定理（对于拓扑空间和 TOP-REAL n） 无参考。

推论 无参考。

推论（对于拓扑空间和 TOP-REAL n） 无参考。

2.21 例子 无参考。（详细列表此处省略。）

2.22 定理 是SETFAM_1:33或TOPS_2:6. 对偶是SETFAM_1:34或TOPS_2:7.

2.23 定理 无参考。

2.23 定理（对于拓扑空间） 是TOPS_1:4.

推论 无参考。

推论（对于拓扑空间） 是TOPS_1:3.

2.24 定理
(a) 没有参考。
(b) 没有参考。
（c）没有参考。
（d）没有参考。

2.24 定理（对于拓扑空间）
（a）是TOPS_2:19.
(b) 是TOPS_2:22.
中的反义词TOPS_2:20.
（d）是TOPS_2:21.

2.25 例子 无参考。

2.26 定义 无参考。

2.26 定义（对于拓扑空间） ${\overline {E}}$ 是Cl E (PRE_TOPC:def 7), 定义是TOPGEN_1:29.

2.27 定理
(a) 没有参考。
(b) 没有参考。
（c）没有参考。

2.27 定理（对于拓扑空间）
(a) 在TOPS_1.
(b) 是PRE_TOPC:22.
中的反义词TOPS_1:5.

2.28 定理 无参考。

2.29 备注 无参考。

2.30 定理 由PRE_TOPC:def 4.

紧集

2.31 定义 是SETFAM_1:def 11.

2.32 定义 无直接参考。紧致在TOPMETR:def 5通过拓扑定义。参见TOPMETR:16.

2.32 定义（对于拓扑空间） 是COMPTS_1:def 1. 有限集是紧致的，集中在YELLOW13.

2.33 定理 无参考。

2.33 定理（对于拓扑空间） 是COMPTS_1:3.

2.35 定理 无参考。

2.35 定理（对于 $T_{2}$ 拓扑空间） 是COMPTS_1:7.

2.35 定理 无参考。

2.35 定理（对于拓扑空间） 是COMPTS_1:8.

推论 无参考。

推论（对于拓扑空间） 无参考。

2.36 定理 无参考。

2.36 定理（对于拓扑空间） 是COMPTS_1:4带有FINSET_1:def 3.

推论 无参考。

推论（对于拓扑空间） 无参考。

2.37 定理 无参考。

2.38 定理 是COUSIN:35.

2.39 定理 无参考。 #TODO 找到嵌套单元的交集非空。

2.40 定理 无参考。 #TODO 找到单元是紧致的。

2.41 定理 无参考。 #TODO 找到 $R^{k}$ 的 Heine-Borel 定理，累积点变体。

2.42 定理 无参考。 #TODO 找到 $R^{k}$ 的 Weierstrass 定理，累积点变体。

2.43 定理 无参考。 #TODO 找到 $R^{k}$ 的非空完备子集是不可数的。

推论 无参考，尽管 $R$ 是不可数的，在定理 2.14 的注释中已经讨论过。 #TODO 实数区间是不可数的。

2.44 康托尔集 参见CANTOR_1. 似乎the_Cantor_set (CANTOR_1:def 5) 的定义并非设计为实数的子集。

连通集

2.45 定义 无参考。

2.45 定义（对于拓扑空间） 是CONNSP_1:def 1和CONNSP_1:def 3.

2.46 备注 是CONNSP_1:1. 一个与书中给出的例子非常相似的例子是BORSUK_4:17.

2.47 定理
前两个聚类。pathwise_connected -> connected在BORSUK_2, interval -> pathwise_connected在TOPALG_2. 现在一个interval具有所描述的属性（XXREAL_2:80) 并且给定的属性描述了interval (XXREAL_2:84)。 注意XXREAL_2:def 12和TOPALG_2:def 3.

习题

1. 是XBOOLE_1:2.
2. 代数数通过ALGNUM_1:def 2和ALGNUM_1:def 4. #TODO 找到代数数集是可数的。
3. 的存在liouville (LIOUVIL1:def 5) 数集中在LIOUVIL1. 超越数被引入为反义词，在ALGNUM_1, liouville 数被聚类为超越数，在LIOUVIL2.
4. 无参考。 #TODO 找到无理数的基数为连续统。
5. 无参考。
6. 度量空间无参考，因为 $E'$ 无参考。 如果拓扑空间是 $T_{1}$, $E'$ 是闭合的（集中在TOPGEN_1), $E''\subset E'$ (TOPGEN_1:32) 和 ${\overline {E'}}=E'$ (TOPGEN_1:33). 没有关于 $E'={\overline {E}}'$ 或 $E'\neq E''$ 的例子。
7. 没有关于度量空间的参考。对于拓扑空间，没有关于有限版本的参考（除了PRE_TOPC:20), 无限版本是TDLAT_2:15.
8. 没有参考。9. 没有关于度量空间的参考。对于拓扑空间，$E^{\circ }$ 是Int E (TOPS_1:def 1), 见上文。
9(a) $E^{\circ }$ 开集在TOPS_1.
9(b) 是TOPS_1:23.
9(c) 是TOPS_1:24.
9(d) 是TOPS_1:def 1.
9(e) 是超稠密 (ISOMICHI:def 1).
9(f) 是亚稠密 (ISOMICHI:def 2).
10. 是METRIC_1:def 10/11. 没有关于开集/闭集/紧集的参考。
11. 没有参考。
12. 没有参考。
13. 没有参考。
14. 没有参考。
15. 没有参考。
16. 没有参考。
17. 没有参考。
18. 没有参考。
19. 没有关于度量空间的参考。对于拓扑空间
19(a) 是CONNSP_1:2.
19(b) 如果 $A\cup B$ 是整个空间，CONNSP_1:3.
19(c) 没有参考。
19(d) 没有参考。
20. 没有参考。
21(a) 没有参考。
21(b) 没有参考。
21(c) 没有参考。
21(d) 没有参考。
22. 没有关于度量空间的参考。可分离由TOPGEN_1:def 12和TOPGEN_1:def 13. $R^{k}$ 的可分离性由一系列簇给出。TOP-REAL k是簇第二可数 (WAYBEL23:def 6) 在MFOLD_0. 第二可数 -> 林德洛夫 (METRIZTS:def 2) 在METRIZTS. 林德洛夫 -> 可分离在METRIZTS如果拓扑空间是可度量化的。没有关于TOP-SPACE k是可度量化 (PCOMPS_1:def 8).
23. 没有关于度量空间的参考。基拓扑空间的基在CANTOR_1. 没有关于该陈述的参考。#TODO 找到每个可分离度量空间都有可数基的证明。
24. 没有参考。
25. 没有参考。
26. 没有参考。
27. 没有关于度量空间的参考。拓扑空间的凝聚点在TOPGEN_4:def 9.凝聚点集定义在TOPGEN_4:def 10. 没有关于该陈述的参考。
28. 没有参考。
29. 没有参考。
30. 没有参考。