Walter Rudin 的《數學分析原理》/連續性 的 Mizar 註釋

函式的極限

4.1 定義
對於由以下給出的實數LIMFUNC3:28. 否則無參考。

4.2 定理
對於實數lim(f,p)在以下定義LIMFUNC3:def 4. 否則無參考。

推論
由以下給出唯一性屬性lim(f,p).

4.3 定義
$f+g$, $f-g$, $fg$ 和 $f/g$ 由以下給出VALUED_1:def 1, VALUED_1:def 9, VALUED_1:def 4和 [VALUED_1:def 10或RFUNCT_1:def 1(前者將 0 的逆對映到 0，後者從定義域中移除這些) 分別。f 是常數在以下定義FUNCT_1:def 10, $f=c$ 是E --> c (FUNCOP_1:def 2), 叢集在VALUED_0. $f\geq g$ 在以下定義COUSIN2:def 3. 函式加法產生復向量由以下給出INTEGR15:def 9和VALUED_2:def 45, 分量乘以VALUED_2:def 47. 向量的聚類在以下給出TOPREALC. 標量乘法由以下給出VALUED_1:def 5, 在同一檔案中具有正確的聚類。

4.4 定理
對於實數
(a) 是LIMFUNC3:33.
(b) 是LIMFUNC3:38.
(c) 是LIMFUNC3:39.
否則無參考。

備註 無參考。

連續函式

4.5 定義
拓撲空間之間函式在一點處的連續性在以下定義TMAP_1:def 2, 在整個定義域中定義在TMAP_1:44(另見PRE_TOPC:def 6). 度量空間無參考。
對於由以下給出的實函式FCONT_1:3在一點處，以及由FCONT_1:def 2對於整個定義域。
對於由以下給出的複函式CFCONT_1:32在一點處，以及由FCONT_1:def 2對於一個定義域。
對於實向量由以下給出NFCONT_1:7(另見PDIFF_7:def 6) 在一點處，以及由NFCONT_1:def 7對於一個定義域。

4.6 定理
無直接參考，從精神上講由 4.5 下面引用的定理結合使用序列的定義給出 (參見FCONT_1:def 1, CFCONT_1:def 1和NFCONT_1:def 5).

4.7 定理
對於由以下給出的拓撲空間TMAP_1:47(逐點) 和TOPS_2:46(整個定義域)。
對於由以下給出的實函式FCONT_1:12(逐點) 並聚類在整個定義域中。
否則無參考。

4.8 定理
對於由以下給出的拓撲空間TOPS_2:43. 對於實函式和實向量僅在鄰域變體中給出 (FCONT_1:5和NFCONT_1:9(後者僅逐點)。 否則無參考。

推論 由原始定義給出PRE_TOPC:def 6對於拓撲空間，否則無參考。

4.9 定理
對於由以下給出的實函式FCONT_1:7和FCONT_1:11(逐點) 並聚類在那裡，除了 $f/g$ (FCONT_1:24) (整個定義域)。
對於由以下給出的複函式CFCONT_1:33和CFCONT_1:37(逐點) 並由CFCONT_1:43和CFCONT_1:49在定義域上。

4.10 定理
(a) 僅當度量空間是 $R$ 時的特例在NFCONT_4:43.
(b) 僅在以下新增NFCONT_1:15.

4.11 例子
投影在以下定義PDIFF_1:def 1. 一般多項式或有理函式的連續性無參考。 $|x|$ 由以下給出NFCONT_1:17(逐點) 和NFCONT_1:28(定義域)。

4.12 備註 無需形式化。

連續性和緊緻性

4.13 定義
對於由以下給出的實函式RFUNCT_1:72, 對於由以下給出的複函式SEQ_2:def 5

. 對於隱式給定的到 $R^{k}$ 的函式INTEGR19:14(左側有界來自INTEGR15:def 12) 它基本上使用了最大範數（比較NFCONT_4:def 2）。沒有關於歐幾里得範數的直接引用。

4.14 定理
對於更一般地由以下給出的拓撲空間COMPTS_1:15或WEIERSTR:8. 對於由以下給出的實函式FCONT_1:29, 對於由以下給出的複函式CFCONT_1:52. 對於由以下給出的實向量NFCONT_1:32.

4.15 定理
在PSCOMP_1中透過使用拓撲空間的偽緊性進行聚類（PSCOMP_1:def 4）。沒有關於度量空間的引用。對於由以下直接給出的實域INTEGRA5:10.

4.16 定理
在PSCOMP_1中透過使用拓撲空間的偽緊性進行聚類（PSCOMP_1:def 4), 同樣。也沒有關於度量空間的引用。對於由以下直接給出的實域FCONT_1:30.

4.17 定理 沒有引用。對於實函式的下一個最佳變體將是FCONT_3:22.

4.18 定義
對於由以下給出的度量空間UNIFORM1:def 1. 對於由以下給出的實函式FCONT_2:def 1. 對於由以下給出的向量NFCONT_2:def 1, 也見INTEGR20:def 1以及以下的定義NCFCONT2.
一致連續函式是連續的，這一點由以下給出UNIFORM1:5對於度量空間（間接），由FCONT_2:9對於實函式，以及由NFCONT_2:7對於向量。

4.19 定理
對於由以下間接給出的度量空間UNIFORM1:7. 對於由以下給出的實函式FCONT_2:11, 對於由以下給出的向量NFCONT_2:10.

4.20 定理
(a) 沒有引用。
(b) 沒有引用。
(c) 沒有引用。

4.21 例子
$f(2\pi t)$ 作為定義在實數線上的函式由以下給出CircleMap在TOPREALB:def 11中。該函式的連續性及其滿射性和單射性（後者僅在長度為 1 的半開區間上受限）也在此處聚類。沒有關於逆函式明確不連續的引用。

連續性和連通性

4.22 定理
更一般地，由以下給出拓撲空間TOPS_2:61. 沒有專門針對實函式的引用。

4.23 定理
TOPREAL5:8, 廣義版本是TOPREAL5:5. 沒有使用簡單實函式的版本的引用。#TODO 找到中間值定理的簡單版本。

4.24 例子 沒有引用。

間斷點

4.25 定義
$f(x\pm )$ 是lim_right/left(f,x) (LIMFUNC2:def 8/7）。“很明顯”是LIMFUNC3:29/30.

4.26 定義
沒有直接引用，儘管間接給出了屬性：$f$ 在 $x$ 處具有第一類間斷點意味著not f is_convergent_in x & f is_left_convergent_in x & f is_right_convergent_in x; $f$ 在 $x$ 處具有第二類間斷點意味著not f is_left_convergent_in x or not f is_right_convergent_in x.

4.27 例子
(a) $f$ 由以下給出(REAL --> 1) - chi(RAT,REAL)(見FUNCOP_1:def 2和FUNCT_3:def 3）。沒有關於間斷性屬性的引用。
(b) $f$ 由以下給出(id REAL)*((REAL --> 1) - chi(RAT,REAL))(另外參見 RELAT_1:def 10 和 FUNCT_1 中的功能屬性FUNCT_1）。沒有關於間斷性屬性的引用。
(c) 沒有引用。
(d) $f$ 由以下給出sin((id REAL)^) +* (0 .--> 0)(見SIN_COS:def 16, RFUNCT_1:def 2, FUNCT_4:def 1和FUNCOP_1:def 9）。沒有關於間斷性屬性的引用。

單調函式

4.28 定義
單調遞增/遞減是非遞減/遞增 (VALUED_0:def 15/16）。該單調屬性在RFUNCT_2:def 5.

4.29 定理 沒有引用，儘管FCONT_3充滿了相關結果。

推論 沒有引用。

4.30 定理 沒有引用。#TODO 找到單調函式間斷點數最多可數的證明。

4.31 備註 沒有引用。

無限極限和無窮大處的極限

4.32 定義 沒有引用，儘管 Mizar 中定義了帶有無窮大的開區間。

4.33 定義
無窮大處的極限被明確地形式化為lim_in+infty f和lim_in-infty f (LIMFUNC1:def 12/13).

4.34 定理
唯一性再次由定義的屬性給出LIMFUNC1:def 12/13. $f+g$, $fg$ 和 $f/g$ 由以下給出LIMFUNC1:82/91, LIMFUNC1:87/96和LIMFUNC1:88/97分別。

練習

1. 無參考。
2. 無參考，包括反向方向的無反例。#TODO 證明$f({\overline {E}})\subset {\overline {f(E)}}$。
3. $Z(f)$ 通常被稱為f"{0} (FUNCT_1:def 7）。無直接參考，但即使按照 Mizar 標準也很明顯。因為PRE_TOPC:def 6我們只需要證明{0}在R^1中是閉集並且我們從聚類得到 (R^1 -> T_2 -> T_1和TOPREAL6PRE_TOPC) 和.
URYSOHN1:19
4. 無參考。#TODO 證明連續函式下稠密集的像是稠密的，並且連續函式由其稠密子集確定。
5. 無參考。基本上是實函式的第 4 題的簡單情況。6. 無參考。由於函式在 Mizar 中是關係，$f$ 由形式為[x,f.x]的元素組成。然而，為了正確嵌入到TOP-REAL 2.
中，需要所有<*x,f.x*> (7. $g$ 被稱為f|E
RELAT_1:def 11
）。無參考。
8. 無參考。
9. 無參考。
10. 無參考。
11. 無參考。
12. 無參考。#TODO 一致連續函式的複合是一致連續的。
15. 13. 無參考。在以下定義14. 無參考。#TODO 連續函式 $f:[0,1]\rightarrow [0,1]$ 的不動點的存在性。開集
T_0TOPSP:def 2）。無參考。 (16. $[x]$ 是[\x/]INT_1:def 6 ()，$(x)$ 是frac x
INT_1:def 8
）。無參考。
17. 無參考。
18. 無參考。19. 無參考。 (20. $\rho _{E}(x)$ 由dist(x,E)SEQ_4:def 17（復向量），
JORDAN1K:def 2（實向量）給出。無參考。和20.(a) 無參考，但參見.
SEQ_4:116
JORDAN1K:45
20.(b) 無參考。21. 無參考。22. 無參考。.
23. 無參考。關於凸性，參見
CONVFUN1:4
24. 無參考。