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. 无参考。