Walter Rudin 的《数学分析原理》/多元函数 - Mizar 注释

线性变换

9.1 定义
(a) 比较 1.36 定义（对于向量空间）。除此之外，REAL-NS n作为赋范空间在REAL_NS1:def 4中定义，TOP-REAL n作为拓扑空间在EUCLID:def 8中定义。（还有REAL-US n (REAL_NS1:def 6）。请注意，这些不是VectSp（比较NORMSTR (NORMSP_1), RLTopStruct (RLTOPSP1）和ModuleStr (VECTSP_1）在第二个图这里）。RLSStruct (RLVECT_1）被并入两者中，NORMSTR中定义，RLTopStruct并为这两种变体提供了大部分属性。RLS 可以被视为 Real Linear Scalar 的缩写。该RLSStruct变体的REAL n (EUCLID:def 1）将是RealVectSpace(Seg n) (FUNCSDOM:def 6中定义，FINSEQ_1:def 1）。请注意，存在CLSStruct (CLVECT_1），这里将不讨论。
(b) 一个Linear_Combination的 $R^{k}$（RLVECT_2:def 3）被定义为一个函数，将向量映射到它们相关的标量。Lin(S) (RLVECT_3:def 2）是 $S$ 的生成子空间。更一般地，一个Linear_Combination向量空间的生成子空间在VECTSP_6:def 1中定义，Lin(S)中定义，在VECTSP_7:def 2.
(c) 线性无关性在RLVECT_3:def 1中定义，或者更一般地在VECTSP_7:def 1.
(d)dim X在RLVECT_5:def 2中定义，或者更一般地在VECTSP_9:def 1中定义。该备注由RLVECT_5:32或VECTSP_9:29.
(e) 该Basis of X在RLVECT_3:def 3中定义，或者更一般地在VECTSP_7通过VECTSP_7:def 3定义。没有关于备注或标准基的参考。

9.2 定理 没有参考。

推论 是EUCLID_7:46对于RealVectSpace(Seg n), RLAFFIN3:4对于TOP-REAL n中定义，EUCLID_7:51对于REAL-US n，否则没有参考。

9.3 定理
(a) 没有参考，但参见RLVECT_5:29.
(b) 由基的定义的存在性（参见(c) 由RLVECT_3:def 3).
RLVECT_3:26RLVECT_5:2或9.4 定义.

对于
$A$ 是一个VectSp 线性变换RANKNULL (）如果它是一个加法VECTSP_1:def 19 (齐次), MOD_2:def 2 (）函数。实线性空间
$A$ 是一个线性算子 线性变换LOPBAN_1 (LOPBAN_1:def 5加法VECTSP_1:def 19 (齐次), MOD_2:def 2 (9.5 定理 没有参考。实线性空间

9.6 定义

(a) 对于
$L(X,Y)$ 是线性算子 LinearOperators(X,Y)LOPBAN_1:def 6 (），没有参考。从 $X$ 到 $Y$ 的函数的加法通常由VectSpFuncAdd(X,Y)LOPBAN_1:def 1 (给出，但也参见FUNCT_3:def 7FUNCOP_1:def 3, 以及在FUNCSDOM中后者的重新定义，以理解定义；或者查看LOPBAN_1:1）。函数的标量乘法仅对由线性算子FuncExtMult(X,Y)LOPBAN_1:def 2 (给出，否则没有参考。(b) 合成已经在
RELAT_1:def 8中定义。合成的加法性在GRCAT_1中集中（另见GRCAT_1:7）。合成的齐次性仅针对在中定义的合成给出，由）函数。MOD_2:2给出，否则没有参考。但是，对于的组合由线性算子LOPBAN_2:1给出.
(c) 对于两个实赋范空间 (NORMSP_1）之间的有界算子 $A$（$X$ 和 $Y$），范数 $||A||$ 由BoundedLinearOperatorsNorm(X,Y).A (LOPBAN_1:def 13给出，在打包到R_NormSpace_of_BoundedLinearOperators (LOPBAN_1:def 14）之前。第一个不等式由LOPBAN_1:32给出，第二个不等式没有参考。没有关于VectSp的参考。

9.7 定理（对于 VectSp） 没有参考。

9.7 定理（对于实赋范空间)
(a) 第一部分由LOPBAN_1:27隐式给出，第二部分由LOPBAN_8:3.
给出(b) 第一部分是LOPBAN_1:37。距离函数通常由NORMSP_2:def 1给出，生成的度量空间由.
NORMSP_2:def 2给出.

(c) 是

LOPBAN_2:2

9.8 定理 没有参考。

9.10 预备知识
关于微分的新视角是Mizar首先提出的，参见5.1 定义以及FDIFF_1.

9.11 定义
符号与实函数的微分相同
$f$ 在 $x$ 处可微意味着f is_differentiable_in x (NDIFF_1:def 6), $f'(x)$ 为diff(f,x) (NDIFF_1:def 7). $f$ 在 $E$ 上可微意味着f is_differentiable_on E (NDIFF_1:def 8), $f'$ 为f`|E (NDIFF_1:def 9). 也请参见PDIFF_1:def 7/8.

9.12 定理由以下给出唯一性性质NDIFF_1:def 7.

9.13 备注
(a) 基本由以下给出NDIFF_1:47.
(b) 由以下类型给出NDIFF_1:def 7中定义，NDIFF_1:def 9.
NORMSP_2:def 2NDIFF_1:44/45.
(d) 无需形式化。

9.14 例子 无参考，但NDIFF_1:43类似。

9.15 定理为NDIFF_2:13.

9.16 偏导数
$(D_{j}f_{i})(x)$ 为partdiff(f,x,j,i) (PDIFF_1:def 16). 使用e_j中定义，u_i被避免，使用reproj(j,x) (PDIFF_1:def 5/6）和Proj(i,m) (PDIFF_1:def 4) 分别替代。

9.17 定理 无参考。

9.18 例子 无参考。

9.19 定理 无参考。

推论 无参考。

9.20 定义 无参考。

9.21 定理为PDIFF_8:20-22.

压缩映射原理

9.22 定义为ALI2:def 1对于MetrSpace中定义，NFCONT_2:def 3对于NORMSTR.

9.23 定理为ALI2:1对于MetrSpace中定义，NFCONT_2:14对于RealBanachSpace.

反函数定理

9.24 定理 无参考。

9.25 定理 无参考。

隐函数定理

9.26 符号

9.27 定理

9.28 定理

9.29 例子 无参考。