# 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 $R^{k}$ (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 $S$. 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 $A$ is a linear-transformation (RANKNULL) if it is a additive (VECTSP_1:def 19), homogeneous (MOD_2:def 2) function. For RealLinearSpace $A$ 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 $L(X,Y)$ is LinearOperators(X,Y) (LOPBAN_1:def 6), no reference fro VectSp. The addition of functions from $X$ to $Y$ 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 $A$ between two RealNormSpace (NORMSP_1) $X$ and $Y$ the norm $||A||$ 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: $f$ is differentiable at $x$ means f is_differentiable_in x (NDIFF_1:def 6), $f'(x)$ is diff(f,x) (NDIFF_1:def 7). $f$ is differentiable on $E$ means f is_differentiable_on E (NDIFF_1:def 8), $f'$ 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 $(D_{j}f_{i})(x)$ 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.