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

*16 April 2019*. There is 1 pending change awaiting review.

## Linear Transformations[edit]

**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[edit]

**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[edit]

**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[edit]

**9.24 Theorem** No reference.

**9.25 Theorem** No reference.

## The Implicit Function Theorem[edit]

**9.26 Notation**

**9.27 Theorem**

**9.28 Theorem**

**9.29 Example** No reference.