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 例子 無參考。