米澤對 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. 沒有參考。