Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Functions of Several Variables

Linear Transformations 9.1 Definition (a) Compare 1.36 Definitions (for vector spaces). Aside from that, REAL-NS n as a normed space is defined in REAL_NS1:def 4 and TOP-REAL n as a topological space is defined in EUCLID:def 8. (There is also REAL-US n (REAL_NS1:def 6).) Note that these are not a VectSp (compare NORMSTR (NORMSP_1), RLTopStruct (RLTOPSP1) and ModuleStr (VECTSP_1) in the second diagram here). RLSStruct (RLVECT_1) is incorporated into both NORMSTR and RLTopStruct and delivers most properties for both variants. RLS can be seen as a abbreviation of Real Linear Scalar. The RLSStruct variant of REAL n (EUCLID:def 1) would be RealVectSpace(Seg n) (FUNCSDOM:def 6 and FINSEQ_1:def 1). Note that there is CLSStruct (CLVECT_1) which will not be discussed here. (b) A Linear_Combination of (RLVECT_2:def 3) is given as a function, sending the vectors to their associated scalars. Lin(S) (RLVECT_3:def 2) is the span of . More generally, a Linear_Combination of a vector space is defined in VECTSP_6:def 1 and Lin(S) in VECTSP_7:def 2. (c) Lineary independence is defined in RLVECT_3:def 1 or more generally in VECTSP_7:def 1. (d) dim X is defined in RLVECT_5:def 2 or more generally in VECTSP_9:def 1. The remark is given by RLVECT_5:32 or VECTSP_9:29. (e) The Basis of X is defined in RLVECT_3:def 3 or more generally in VECTSP_7 via VECTSP_7:def 3. No reference for the remark or the standard basis. 9.2 Theorem No reference. Corollary is EUCLID_7:46 for RealVectSpace(Seg n), RLAFFIN3:4 for TOP-REAL n and EUCLID_7:51 for REAL-US n, else no reference. 9.3 Theorem (a) No reference, but see RLVECT_5:29. (b) is given by existence property of the definition of a basis (see RLVECT_3:def 3). (c) is given by RLVECT_3:26 or RLVECT_5:2. 9.4 Definition For VectSp is a linear-transformation (RANKNULL) if it is a additive (VECTSP_1:def 19), homogeneous (MOD_2:def 2) function. For RealLinearSpace is a LinearOperator (LOPBAN_1) if it is a additive (VECTSP_1:def 19), homogeneous (LOPBAN_1:def 5) function. 9.5 Theorem No reference. 9.6 Definitions (a) For RealLinearSpace is LinearOperators(X,Y) (LOPBAN_1:def 6), no reference fro VectSp. The addition of functions from to is generally given by FuncAdd(X,Y) (LOPBAN_1:def 1, but also see FUNCT_3:def 7, FUNCOP_1:def 3 and the redefinition of the latter in FUNCSDOM to understand the definition; or look at LOPBAN_1:1). Skalar multiplication of functions is only given for RealLinearSpace by FuncExtMult(X,Y) (LOPBAN_1:def 2), else no reference. (b) Composition was already defined RELAT_1:def 8. Additivity of the composition is clustered in GRCAT_1 (see also GRCAT_1:7). Homogeneity of the composition is only given for the one defined in MOD_2:def 2, given by MOD_2:2, else no reference. However, the combination for RealLinearSpace is given by LOPBAN_2:1. (c) For a bounded operator between two RealNormSpace (NORMSP_1) and the norm is given by BoundedLinearOperatorsNorm(X,Y).A (LOPBAN_1:def 13), before it is packed into R_NormSpace_of_BoundedLinearOperators (LOPBAN_1:def 14). The first inequality is given by LOPBAN_1:32, no reference for the second inequality. No reference for VectSp either. 9.7 Theorem (for VectSp) No reference. 9.7 Theorem (for RealNormSpace) (a) The first part is given implicitly by LOPBAN_1:27, the second one is given by LOPBAN_8:3. (b) First part is LOPBAN_1:37. The distance function is generally given by NORMSP_2:def 1 and the generated metric space by NORMSP_2:def 2. (c) is LOPBAN_2:2. 9.8 Theorem No reference. 9.9 Matrices No reference. Differentiation 9.10 Preliminaries The new viewpoint on differentiation is the one Mizar starts with, see 5.1 Definition and FDIFF_1. 9.11 Definition The notations are the same as for differentiation of real functions: is differentiable at means f is_differentiable_in x (NDIFF_1:def 6), is diff(f,x) (NDIFF_1:def 7). is differentiable on means f is_differentiable_on E (NDIFF_1:def 8), is f`|E (NDIFF_1:def 9). See also PDIFF_1:def 7/8. 9.12 Theorem is given by the uniqueness property of NDIFF_1:def 7. 9.13 Remark (a) Basically given by NDIFF_1:47. (b) Given by the types of NDIFF_1:def 7 and NDIFF_1:def 9. (c) is NDIFF_1:44/45. (d) Nothing to formalize. 9.14 Example No reference, but NDIFF_1:43 is similar. 9.15 Theorem is NDIFF_2:13. 9.16 Partial derivates is partdiff(f,x,j,i) (PDIFF_1:def 16). The use of e_j and u_i is avoided by using reproj(j,x) (PDIFF_1:def 5/6) and Proj(i,m) (PDIFF_1:def 4) respectively. 9.17 Theorem No reference. 9.18 Example No reference. 9.19 Theorem No reference. Corollary No reference. 9.20 Definition No reference. 9.21 Theorem is PDIFF_8:20-22. The Contraction Principle 9.22 Definition is ALI2:def 1 for MetrSpace and NFCONT_2:def 3 for NORMSTR. 9.23 Theorem is ALI2:1 for MetrSpace and NFCONT_2:14 for RealBanachSpace. The Inverse Function Theorem 9.24 Theorem No reference. 9.25 Theorem No reference. The Implicit Function Theorem 9.26 Notation 9.27 Theorem 9.28 Theorem 9.29 Example No reference.