Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Printable version

The Mizar system consists of three parts: a formal language to write mathematical proofs in, a programm to check these proofs for correctness automatically and the Mizar Mathematical Library (MML). The MML has gotten quite large since its founding in 1989 and therein lies a small problem:

The most difficult part of writing Mizar is finding what you need in the MML which is the name of the Mizar Mathematical Library. Unfortunately that problem has no easy solution. You will discover that apart from that, writing a Mizar article is straight-forward.

—F. Wiedijk, Writing a Mizar article in nine easy steps

This book is an attempt to overcome this problem. We've selected the well known classic analysis book Principles of Mathematical Analysis ("the Book" within this book) written by Walter Rudin and wrote down where to find the definitions and theorems of the Book in the MML. If mathematical concepts differ between the Book and the MML, this is explained as well where appropriate. For example, in the Book it isn't explained what exactly a relation is, but rather what a function and (later) equivalence relation is, while both are a special kind of relation in Mizar.

Of course, since the MML doesn't contain all of mathematics, some definitions or theorems may have not been formalized yet. Additionally, as Wiedijk wrote, it is not necessarily easy to search the MML for a specific statement, so the authors of this book could have simply overlooked it despite their efforts. So if a statement is commented with "no reference" it means "no reference found".

For this book, the third edition of the Book and version 5.54.1341 of the MML are used, unless otherwise stated.

Introduction

The familiarity with the rational numbers as described in the Book can be found in RAT_1.

1.1 Example Proven more generally in IRRAT_1:1. No reference for the closer examination, but the idea of it will return with the Dedekind cuts.

1.2 Remark

• for r, s being Rational st r < s ex x being irrational Real st r < x & x < s No reference.
• for r, s being Rational st r < s ex x being Rational st r < x & x < s No reference.

1.3 Definitions
$x\in A$ is x in A from HIDDEN (and therefore always present without reference). $x\notin A$ is usually written as not x in A; nevertheless x nin A is introduced as antonym in XBOOLE_0.
The empty set is denoted by {} (XBOOLE_0:def 2) and the property of a set being empty by empty (XBOOLE_0:def 1), therefore the property of a set to be nonempty is non empty. With the usual requirements the term A = {} is evaluated just like A is empty.
$A\subset B$ is A c= B (TARSKI:def 3), there is no reference for $B\supset A$. $A$ being a proper Subset of $B$ (SUBSET_1:def 6) can also be written as A c< B (XBOOLE_0:def 8). $A\subset A$ is given by the reflexivity property of c= in TARSKI:def 3.
$A=B$ is redefined in XBOOLE_0:def 10, $x\neq y$ is generally introduced as an antonym in HIDDEN.

1.4 Definition $Q$ is RAT (defined in NUMBERS:def 3, redefined in RAT_1:def 1).

Ordered Sets

The term "relation" is used in the Book without an explanation. A Relation is defined as a Relation-like set (RELAT_1), a Relation of X,Y is defined as a Subset of [:X,Y:] (RELSET_1), where [:X,Y:] is the cartesian product of $X$ and $Y$ (ZFMISC_1:def 2). Many properties of relations are introduced in RELAT_2.

1.5 Definition The order on $S$ is defined as a (i) total (PARTFUN1:def 2) connected (RELAT_2:def 14) ["one"], asymmetric (RELAT_2:def 13) ["and only one"] (ii) transitive (RELAT_2:def 16) Relation on S. Note that in Mizar an Order of S (from ORDERS_1) is defined as a total reflexive (RELAT_2:def 9) antisymmetric (RELAT_2:def 12) transitive Relation on S. If S is connected additionally, then in Mizar S is being_linear-order (ORDERS_1:def 6).

let S be set, R be Relation of S, x,y be object; Instead of x < y we would write [x,y] in R (see also RELAT_1), but the < notation can be archived with the following notation.

1.6 Definition A set equipped with a relation is a RelStr (ORDERS_2). let S be RelStr, then the underlying set is denoted by the carrier of S (see STRUCT_0), and the relation is the InternalRel of S. let a, b be Element of S. Then $a\leq b$ is denoted by a <= b (ORDERS_2:def 5) and $a<b$ is a < b (ORDERS_2:def 6). In this sense, a LinearOrder (ORDERS_5) is an ordered set as defined in the Book.
No reference for $Q$ being an ordered set.

1.7 Definition Bounded below/above is lower/upper-bounded (YELLOW_0:def 4/5, see also LATTICE3:def 8/9). No reference for lower/upper bound.

1.8 Definition The described properties are encoded as the predicate ex_sup/inf_of in YELLOW_0:def 7/8. No reference for sup/inf.

1.5-1.8 Definition (with reals)
$x\leq y$ is defined as x <= y (XXREAL_0:def 5) for extended reals, the other variants are given by notations. Antisymmetry is XXREAL_0:1, transitivity is XXREAL_0:2 and a lot of inequalities are given in XREAL_1.
All sets of extended reals have an upper and lower bound (and a least variant of it) in form of an extended real. Upper/LowerBound are defined in XXREAL_2:def 1/2. sup/inf are defined in XXREAL_2:def 3/4, and again as upper/lower_bound (SEQ_4:def 1/2) for upper/lower bounded sets of reals (identified with each other in RINFSUP2:1-4). A set of extended reals is bounded_above/below (XXREAL_2:def 9/10) if there is a real upper/lower bound.

1.9 Examples
(a) No reference, since no reference for refinement in Example 1.1.
(b) No reference.
(c) No reference.

1.10 Definition No reference.

1.11 Theorem The set of all upper/lower bounds of a set $B$ of extended reals is denoted by SetMajorant/Minorant(B) (SUPINF_1:def 1/2). Then the theorem is proven by SUPINF_1:3. No reference for general case.

Fields

Like most algebraic structures, a Field (VECTSP_1) in Mizar is built up from its components. The basic structure of a field is that of a doubleLoopStr (ALGSTR_0), i.e. a set equipped with two binary operations and a One and a Zero. The additional attributes of a Field are to be commutative (GROUP_1:def 12) non degenerated (STRUCT_0:def 8) almost_left_invertible (VECTSP_1:def 9) Abelian (RLVECT_1:def 2) add-associative (RLVECT_1:def 3) right_zeroed (RLVECT_1:def 4) right_complementable (ALGSTR_0:def 11) associative (GROUP_1:def 3) well-unital (VECTSP_1:def 6) distributive (VECTSP_1:def 7) non empty (STRUCT_0:def 1).

1.12 Definition
(A1) and (M1) are encoded by mode BinOp from BINOP_1.
(A2) means Abian (RLVECT_1:def 2).
(A3) means add-associative (RLVECT_1:def 3).
(A4) is given by the basic structure, right_zeroed (RLVECT_1:def 4) and the commutativity of the addition.
(A5) means right_complementable (ALGSTR_0:def 11 and ALGSTR_0:def 13).
(M2) means commutative (GROUP_1:def 12).
(M3) means associative (GROUP_1:def 3).
(M4) is given by the basic structure, non degenerated (STRUCT_0:def 8) and well-unital (VECTSP_1:def 6).
(M5) means almost_left_invertible (VECTSP_1:def 9 and VECTSP_1:def 9 and VECTSP_1:def 10).
(D) means distributive (VECTSP_1:def 7).

1.12 Definition (with complex numbers)
(A1) and (M1): The binary operations are given as functors rather than functions in XCMPLX_0:def 4/5. Their closure is clustered in XCMPLX_0, XREAL_0, RAT_1, INT_1 and NAT_1 for complex, real, rational, integer and natural numbers respectively.
(A2) and (M2) are encoded in the definitions of the functors directly in XCMPLX_0.
(A3) and (M3) are XCMPLX_1:1 and XCMPLX_1:4 respectively, should be used via requirements.
(A4) Existence of $0$ is ORDINAL1:def 13/14; as a member of the complex, real and natural numbers respectively in XCMPLX_0, XREAL_0 and NAT_1. For rational and integer numbers this is at least done indirectly (else no reference) since natural numbers are also rational and integer. $0+x=x$ is finally done in ARITHM:1, which should be included by requirements, not by theorems.
(A5) is XCMPLX_0:def 6.
(M4) $1$, like all other numerals in Mizar, is defined implicitly. CARD_1:49 states $1=\{0\}$, with the irreflexivity property built into in and TARSKI:def 1 one can show that $1\neq 0$ whenever needed, no direct reference. $1x=x$ is ARITHM:3, again to be used via requirements.
(M5) is XCMPLX_0:def 7
(D) is XCMPLX_1:8, should be used via requirements.

1.13 Remarks
(a) $x-y$ is ALGSTR_0:def 14, ${\tfrac {x}{y}}$ is ALGSTR_0:def 43. Functors in Mizar are left-associative, hence x+y+z=(x+y)+z is built in, same for multiplication. $x^{n}$ is x |^ n (GROUP_1:def 9), $x^{2}$, $x^{3}$ are given by GROUP_1:27, GROUP_1:28. $n\times x$ is n * x (GROUP_1A:def 8), $2x$, $3x$ are given by GROUP_1A:26, GROUP_1A:26.
(a) (with complex numbers) $x-y$ is XCMPLX_0:def 8, ${\tfrac {x}{y}}$ is XCMPLX_0:def 9. Both can be exchanged with their definition without any problem given the correct requirements and thanks to XCMPLX_1. Clusterings for subfields etc. are done where the clusterings for addition and multiplication is done (see above). $2x$, $3x$ and $4x$ are in XCMPLX_1 and can be used without a problem. $x^{2}$ is SQUARE_1:def 1, $x^{n}$ is defined in NEWTON:def 1 (for natural $n$), $x^{2}$, $x^{3}$, $x^{4}$ are given in POLYEQ_5:1-3, see also NEWTON:81 and POLYEQ_2:4.
(b) is GAUSSINT:def 14 with GAUSSINT:14.
(c) As you can see above, the field properties are done twice in Mizar, once for the general case and once for complex numbers. However, what is done for the complex numbers is used to show that the complex, real and rational numbers form a field in the general sense (see associated proofs for F_Complex in COMPLFLD, F_Real in VECTSP_1 and F_Rat in GAUSSINT).

1.14 Proposition
(a) is GROUP_1A:6.
(b) is GROUP_1A:7.
(c) is GROUP_1A:5.
(d) is encoded in the involutiveness of GROUP_1A:def 4.

1.14 Proposition (with complex numbers)
(a) is XCMPLX_1:2.
(b) is XCMPLX_1:3.
(c) is encoded in the uniqueness of XCMPLX_0:def 6. For extended reals is XXREAL_3:8.
(d) is encoded in the involutiveness of XCMPLX_0:def 6.

1.15 Proposition
(a) is VECTSP_1:5.
(b) is GCD_1:1.
(c) is encoded in the uniqueness of ALGSTR_0:def 30.
(d) is VECTSP_1:24.

1.15 Proposition (with complex numbers)
(a) is XCMPLX_1:5.
(b) is XCMPLX_1:7.
(c) is encoded in the uniqueness of XCMPLX_0:def 7.
(d) is encoded in the involutiveness of XCMPLX_0:def 7.

1.16 Proposition
(a) is VECTSP_1:7.
(b) is VECTSP_1:12.
(c) is VECTSP_1:8 and VECTSP_1:9.
(d) is VECTSP_1:10.

1.16 Proposition (with complex numbers)
(a) is ARITHM:2.
(b) is XCMPLX_1:6 for one direction, the other one is clustered in XCMPLX_0.
(c) is XCMPLX_1:174 and XCMPLX_1:175.
(d) is XCMPLX_1:176.

1.17 Definition No reference, hence also no reference for $Q$ being an ordered field, except that the properties are present:

1.17 Definition (with reals)
(i) is given by XREAL_1:6 (this works for a < b instead of a <= b because it means not b <= a).
(ii) is given by XREAL_1:129.

The attributes positive/negative are given by XXREAL_0:def 6 and are properly clustered in XREAL_0 for reals.

1.18 Proposition No reference, since ordered fields are not referenced.

1.18 Proposition (with reals)
(a) is XREAL_1:58.
(b) is XREAL_1:68.
(c) is XREAL_1:69.
(d) is XREAL_1:63 or SQUARE_1:12. $1>0$ is built into the appropiate requirements.
(e) is XREAL_1:88 and XREAL_1:122.

The Real Field

1.19 Theorem Existence of $R$ is NUMBERS:def 1, other properties have been shown above. The explanation is mainly GAUSSINT:13.

1.20 Theorem
(a) No reference, closest is SEQ_4:3. #TODO find the archimedean property!
(b) is RAT_1:7.

1.21 Theorem is PREPOWER:def 2, where ${\sqrt[{n}]{x}}$ is written as n -Root x. Also written as n -root x (POWER:def 1). $x^{\tfrac {1}{n}}$ is given by POWER:45.

Corollary is PREPOWER:22 or POWER:11 or more generally POWER:30.

1.22 Decimals No reference (#TODO find it!), although NUMERAL1 introduces at least the representation of naturals to base $b$.

The Extended Real Number System

1.23 Definition
$+\infty$/$-\infty$ are defined in XXREAL_0:def 2/3. $-\infty <x<+\infty$ is XXREAL_0:9 and XXREAL_0:12.
As noted before, the definition of sup/inf in XXREAL_2 guaranties the existence of a least upper/lower bound for any extended real. That $+\infty$/$-\infty$ is an upper/lower bound of any set of extended reals is XXREAL_2:41/42.
(a) are XXREAL_3:def 2, XXREAL_3:13, XXREAL_3:76/77 respectively.
(b) and (c) are XXREAL_3:def 5.
It should be noted that the undefined expressions involving $\pm \infty$ are set to $0$ in Mizar.
A not infinite real is called real (XREAL_0:def 1) in Mizar, a possibly infinite one is called ext-real (XXREAL_0:def 1).

The Complex Field

1.24 Definition
The (mostly used) ordered pair in Mizar is [a,b] (TARSKI:def 5), with the distinction property in XTUPLE_0:1. However, in Mizar the complex numbers consist of the set REAL (NUMBERS:def 1) and functions of the form Funcs({0,1},REAL) (see also FUNCT_2:def 2) where the value of $1$ isn't $0$. This slight sophistication allows a rigorous inclusion REAL c= COMPLEX (NUMBERS:11) instead of an injection from reals into complex numbers thought as inclusion. To work with some kind of pairs nevertheless (until $i$ is introduced), [*a,b*] (ARYTM_0:def 5, see also FUNCT_4:def 4) is used.
Just as for normal ordered pairs, the uniqueness condition of function in Mizar ensures that a=c & b=d implies [*a,b*]=[*c,d*] automatically. The other direction is given by ARYTM_0:10 and, for $i$, by COMPLEX1:77.
Addition/Multiplication is given in XCMPLX_0:def 4/5.

1.25 Theorem
The field properties through the functors have been shown above. The clustering of F_Complex to a Field is done in COMPLFLD.

1.26 Theorem is the clustering done in XREAL_0. Thanks to the definition of [*a,b*] we really have [*a,0*]=a.

1.27 Definition is XCMPLX_0:def 1, $i$ is <i>.

1.28 Theorem is COMPLEX1:18.

1.29 Theorem has no direct reference, but COMPLEX1:12.

'1.30 Definition
${\overline {z}}$ is z*' (COMPLEX1:def 11).
${\mbox{Re}}(z)$/${\mbox{Im}}(z)$ is Re z/Im z (COMPLEX1:def 1/2).

1.31 Theorem
(a) is COMPLEX1:32.
(b) is COMPLEX1:35.
(c) is basically COMPLEX1:41 and COMPLEX1:42.
(d) has no direct reference, COMPLEX1:40 comes closest.

1.32 Definition
$|z|$ is |.z.| (COMPLEX1:def 12, see also SQUARE_1:def 2).
${\overline {x}}=x$ is given as a reduction in COMPLEX1, $|x|={\sqrt {x^{2}}}$ is COMPLEX1:72, the conclusion is COMPLEX1:70/71.

1.33 Theorem
(a) is clustered in COMPLEX1 and also given by COMPLEX1:44/45.
(b) is COMPLEX1:53.
(c) is COMPLEX1:65.
(d) is COMPLEX1:54.
(e) is COMPLEX1:56.

1.34 Notation
To define something like $\Sigma x_{j}$, the notion of tuples is needed. This is done in FINSEQ_1, defining tuples as functions with domain $\{1,\ldots ,n\}$. In RVSUM_1 the existence of complex-valued (VALUED_0:def 1) FinSequence (FINSEQ_1:def 2) is clustered.
let x be complex-valued FinSequence, then $\Sigma x_{j}$ is given by Sum x (RVSUM_1:def 10). Basic properties are in RVSUM_1 for the real-valued case and in RVSUM_2 for the complex-valued case.

1.35 Theorem No direct reference, can be followed from CSSPACE:35 or HERMITAN:46. #TODO find direct reference of Schwarz inequality for complex-valued FinSequences!

Euclidean Spaces

1.36 Definitions
$R^{k}$ is REAL k (EUCLID:def 1, see also FINSEQ_2:def 4).
Addition of vectors is RVSUM_1:def 4, scalar multiplication is RVSUM_1:def 7. The clustering to Elements of REAL k is done in EUCLID.
Commutativity of addition is encoded in RVSUM_1:def 4, associativity is RVSUM_1:15. Associativity for scalar multiplication is RVSUM_1:49. Distributivity laws are RVSUM_1:50 and RVSUM_1:51. k|->(0 qua Real) is the zero vector (see also FINSEQ_2:def 2), its defining property is RVSUM_1:16.
The inner product $x\cdot y$ is |( x,y )| (RVSUM_1:def 16), the norm $x$ is |. x .| (EUCLID:def 5, see also RVSUM_1:def 8), their relation is EUCLID_2:37.
$R^{k}$ as a vector space has no direct reference but is given by RealVectSpace Seg k (compare FUNCSDOM:def 6 and FINSEQ_1:def 1).

1.36 Definitions (for vector spaces)
The book gave the definition of a vector space implicitly. In Mizar, a VectSp is a ModuleStr over a Ring (all defined in VECTSP_1) which is scalar-distributive (VECTSP_1:def 15) vector-distributive (VECTSP_1:def 14) scalar-associative (VECTSP_1:def 16) scalar-unital (VECTSP_1:def 17) add-associative (RLVECT_1:def 3) right_zeroed (RLVECT_1:def 4) right_complementable (ALGSTR_0:def 11) Abelian (RLVECT_1:def 2) non empty (STRUCT_0:def 1).

1.37 Theorem
(a) is EUCLID:9.
(b) is EUCLID:7/8.
(c) is EUCLID:11.
(d) is EUCLID_2:15.
(e) is EUCLID:12.
(f) is EUCLID:19.

1.38 Remarks
As a metric space, $R^{k}$ is Euclid k (EUCLID:def 7). As a topological space, it is TOP-REAL k (EUCLID:def 8). $R^{1}$ as a metric space is also RealSpace (METRIC_1:def 13) and as a topological space is also R^1 (TOPMETR:def 6). Note that the difference is that the underlying set (the carrier) of both RealSpace and R^1 is REAL, while the underlying set of both Euclid 1 and TOP-REAL 1 is Funcs(Seg 1,REAL).

Appendix

It is to be noted that in Mizar, as opposed to the Book, the real numbers are not constructed from the rationals by Dedekind cuts, but rather the non-negative reals are constructed from the nonnegative rationals, and only afterwards the sets of rationals and reals are constructed from their nonnegative part in NUMBERS:def 3 and NUMBERS:def 1 respectively.

Step 1
(II), (III) and the second part of (I) are in the definition of DEDKIND_CUTS (ARYTM_2:def 1). The empty set is not explicitly forbidden, as (I) would indicate, but since the empty set is identified with $0$ this hardly matters. The two properties mentioned can be derived from the definition of DEDEKIND_CUT x (ARYTM_2:def 3). The definition of REAL+ is given immediatly by ARYTM_2:def 2. Just like with the complex numbers, the Dedekind cuts responding to rational numbers are directly excluded and RAT+ is used instead.

Step 2 is given by the predicate x <=' y (ARYTM_2:def 5), the connectedness is wired in there directly. The connectedness for the cuts is given by ARYTM_2:7, too.

Step 3 No reference.

Step 4 Addition of cuts is ARYTM_2:def 6, of nonnegative reals is ARYTM_2:def 8. (A1) and (A2) are wired directly into the definitions. (A3) is ARYTM_2:6. (A4) is given explicitly in ARYTM_2:def 8. (A5) is given via ARYTM_1:def 2 and ARYTM_1:18.

Step 5 is concretly given by ARYTM_1:7.

Step 6 Multiplication of cuts is ARYTM_2:def 7, of nonnegative reals is ARYTM_2:def 9. Again (M1) and (M2) are wired directly into the definitions. (M3) is ARYTM_2:12, (M4) is ARYTM_2:15. (M5) is given only later with reals in ARYTM_0:def 4.

Step 7 Given later by ARYTM_0:def 2 and ARYTM_0:15. Then (D) is ARYTM_0:14. (Just for nonnegative reals it is given by ARYTM_2:13.)

Step 8 $r^{\ast }$ is DEDEKIND_CUT r (DEDEKIND_CUT x). No direct reference for the properties.

Step 9 As mentioned above, we have a direct inclusion by definition ARYTM_2:def 2, made plain by ARYTM_2:1.

Exercises

1. is given by BORSUK_5:18 and BORSUK_5:22. It's clustered in that article as well.
2. implicitly given by IRRAT_1:1, PEPIN:41 and 1. since $12=2^{2}\cdot 3$. No direct reference.
3. given above in Proposition 1.15.
4. implicitly given by XXREAL_2:def 1, XXREAL_2:def 2 and XXREAL_0:2. No direct reference.
5. given by SUPINF_2:15.
6.(a) is corrolary of POWER:33; if that is not given, the proof could be built with PREPOWER (see especially PREPOWER:def 4), but no direct reference.
6.(b) is PREPOWER:53.
6.(c) has no reference. A similar approach is used in PREPOWER:def 7.
6.(d) is PREPOWER:75 or POWER:33.
7.(a) given by POWER:22, more directly POWER:49.
7.(b) is POWER:22.
7.(c)-(g) have no direct reference; existence and uniqueness proofs of $\log$ are done in POWER:def 3.
8. No reference. #TODO Find that COMPLEX cannot be ordered!
9. No reference.
10. No direct reference. Complex roots are defined in POLYEQ_5:def 1, see also POLYEQ_5:11 and POLYEQ_5:12 as well as COMPTRIG:def 2.
11. implicitly given by COMPTRIG:62, no direct reference.
12. No reference. #TODO Find that |.Sum z.| <= Sum |.z.|.
13. is COMPLEX1:64.
14. No reference.
15. No reference for equality, since no reference for normal Schwarz inequality.
16. No reference.
17. is EUCLID_2:13. The variant for real unitary spaces is BHSP_5:5.
18. No reference.
19. No reference.
20. No reference.

Finite, Countable, And Uncountable Sets

As mentioned before, the Book does not properly introduce relations. In Mizar, a function is a special kind of Relation (see RELAT_1:def 1), so many facts that seem obvious about functions hold more generally for relations, and are therefore in RELAT_1 instead of FUNCT_1.

2.1 Definition
A Function $f$ is defined by FUNCT_1:def 1. $f(x)$ is f.x (FUNCT_1:def 2). A Function of A,B is defined in FUNCT_2, it main properties are encoded by FUNCT_2:def 1, RELAT_1:def 18 and RELAT_1:def 19. The domain/range of $f$ dom f/rng f is initially defined in XTUPLE_0:def 12/13 and renamed in RELAT_1. rng f gets a helpful redefinition in FUNCT_1:def 3.

2.2 Definition
$f(E)$ is f.:E (RELAT_1:def 13, FUNCT_1:def 6), the remark is RELAT_1:113. $f(A)\subset B$ is encoded in RELSET_1. Onto is onto (FUNCT_2:def 3).
$f^{-1}(E)$ is f"E (RELAT_1:def 14, FUNCT_1:def 7). $f^{-1}(y)$ is f"{y} or Coim(f,y) (RELAT_1:def 17). There is no reference for the first definition in the Book of "one-to-one", but the second one is FUNCT_1:def 4.

2.3 Definition
The one-to-one correspondence of $A$ and $B$ is expressed by A,B are_equipotent (WELLORD2), that this is equivalent to their cardinality is CARD_1:5. Reflexivity and symmetry are encoded in WELLORD2:def 4, transitivity is WELLORD2:15. On the other hand, reflexivity, symmetry and transitivity of the cardinality are built in by the = predicate.
The properties of a Relation to be reflexive, symmetric and transitive are given by RELAT_2:def 9, RELAT_2:def 11 and RELAT_2:def 16 respectively. Equivalence_Relation is defined in EQREL_1. In Mizar, a Relation is a proper set and since a reflexive relation contains a copy of itself, the one-to-one correspondence of sets cannot be expressed in a Relation in Mizar since there is no set of sets.

2.4 Definition
$J_{n}$ is Seg n (FINSEQ_1:def 1), $J$ is NATPLUS (NAT_LAT:def 6), although it should be mentioned that in Mizar NAT (ORDINAL1:def 11, synonym introduced in NUMBERS) being $J\cup \{0\}$ is more commonly used. Nonnegative integers are usually used with let n be Nat, positive integers with let n be non zero Nat (ORDINAL1:def 14) instead of let n be Element of NATPLUS. Consequently, countability is defined with NAT.
(a) The definition is equivalent to the one in Mizar (FINSET_1:def 1). If X is finite, then $X$ is finite by FINSEQ_1:56. If $X$ is finite, then card X = card Seg n = n by (FINSEQ_1:57), then card X is finite (natural -> finite clustered in CARD_1) and hence X is finite (because for infinite $X$ card X -> infinite is clustered in CARD_1).
(b) is given as antonym of finite in FINSET_1.
(c) is denumerable (CARD_3:def 15).
(d) is given as antonym of countable in CARD_3.
(e) is countable (CARD_3:def 14).

2.5 Example is clustered in GAUSSINT.

2.6 Remark No reference. #TODO Find reference for X is infinite iff ex Y being proper Subset of X st X,Y are_equipotent

2.7 Definition
A function with a certain domain $X$ (but not necessarily a certain range), a ManySortedSet of X is a total X-defined Function (PBOOLE). Then a sequence in Mizar (starting with $0$ instead of $1$) is a ManySortedSet of NAT. If it is a sequence of elements of some $A$, then it can also be described as a sequence of A (NAT_1).
The remark following afterwards is partly encoded in DICKSON:3, but there is no reference.

2.8 Theorem No reference. #TODO Find let X be denumerable set; cluster infinite -> denumerable for Subset of X

2.9 Definition
An indexed set family is a ManySortedSet, as described above. If just a set $E$ of subsets of $\Omega$ is given, that would be a Subset-Family (SETFAM_1). Since any object is a set in Mizar, the functor union E (TARSKI:def 4) works without that notion. $E_{1}\cup E_{2}$ is E1 \/ E2 (XBOOLE_0:def 3). The intersection of $E$ is meet E (SETFAM_1:def 1). $E_{1}\cap E_{2}$ is E1 /\ E2 (XBOOLE_0:def 4). $A$ and $B$ intersect is A meets B (as antonym of the next predicate in XBOOLE_0), else A misses B (XBOOLE_0:def 7).

2.10 Example
(a) No reference.
(b) No reference.

2.11 Remarks
(8) is wired in the definitions XBOOLE_0:def 3/4.
(9) is XBOOLE_1:4 and XBOOLE_1:16.
(10) is XBOOLE_1:23 (and the other one is XBOOLE_1:24).
(11) is XBOOLE_1:7.
(12) is XBOOLE_1:17.
(13) is built in with the correct requirements.
(14) is XBOOLE_1:12 and XBOOLE_1:28.

2.12 Theorem No reference. #TODO Find that union of set family is denumerable if each set in it is at most countable and at least one is denumerable

Corollary is CARD_4:12.

2.13 Theorem is CARD_4:10.

Corollary is TOPGEN_3:17.

2.14 Theorem
TOPGEN_3:29 in combination with CARD_2:def 3 and CARD_1:50 shows that the cardinality of the 0-1-sequences is the same as the cardinality of REAL. TOPGEN_3:30 shows that that the reals are not denumerable.

Metric Spaces

2.15 Definition is MetrSpace (METRIC_1), defined through METRIC_1:def 6-9 (which refer to METRIC_1:def 2-5 respectively).

2.16 Examples
As noted before, $R^{k}$ as a metric space is Euclid n (EUCLID:def 7), $R^{1}$ is also RealSpace (METRIC_1:def 13).
Subsets of $Y$ as metrics spaces is done by SubSpace of Y (TOPMETR:def 1) and TOPMETR:def 2.
#TODO Reference the last two examples.

2.17 Definition
$(a,b)$ is ].a,b.[ (XXREAL_1:def 4), $[a,b]$ is [.a,b.] (XXREAL_1:def 1), $[a,b)$ is [.a,b.[ (XXREAL_1:def 2), $(a,b]$ is ].a,b.] (XXREAL_1:def 3).
A $k$-cell is cell(a,b) (CHAIN_1:def 6).
The open/closed ball with center $x$ and radius $r$ is given by Ball(x,r)/cl_Ball(x,r) (METRIC_1:def 14/15 for metric spaces and TOPREAL9:def 1/2 for TOP-REAL k).
Convex sets are defined by CONVEX1:def 2 (usable for TOP-REAL k, but not for Euclid k). The open/closed balls are clustered as convex in TOPREAL9. No reference for convexity of cells. #TODO Find it.

2.18 Definition
(a) is Ball(p,r) (METRIC_1:def 14)
(b) No reference.
(c) No reference.
(d) No reference.
(e) No reference.
(f) No reference.
(g) No reference.
(h) No reference.
(i) is TBSP_1:def 7 or METRIC_6:def 3.
(j) No reference.

2.18 Definition (for topological spaces and TOP-REAL k)
The basics of topological spaces are in PRE_TOPC.
(a) is Ball(p,r) (TOPREAL9:def 1)
(b) "$p$ is a limit point of $E$" is basically p is_an_accumulation_point_of E (TOPGEN_1:def 2), this is shown with TOPS_1:12. The set of all limit points of $E$, the derivative of $E$, is Der E (TOPGEN_1:def 3), which gives a second characterization via TOPGEN_1:17.
(c) Just like that, "$p$ is a isolated point of $E$" is p is_isolated_in E (TOPGEN_1:def 4).
(d) is TOPGEN_4:3. A set is defined to be closed in PRE_TOPC:def 3.
(e) is TOPS_1:22. The interior of $E$ is Int E (TOPS_1:def 1).
(f) is TOPS_1:23. A set is defined to be open in PRE_TOPC:def 2.
(g) is SUBSET_1:def 4, see also XBOOLE_0:def 5.
(h) is TOPGEN_1:def 10 in combination with TOPGEN_1:def 7. See also TOPS_1:5 and TOPGEN_1:28. (i) No reference.
(j) given by TOPS_1:def 3 and TOPGEN_1:29.

2.19 Theorem No reference.

2.19 Theorem (for topological spaces and TOP-REAL n) the balls of TOP-REAL k are clustered open in TOPREAL9.

2.20 Theorem No reference.

2.20 Theorem (for topological spaces and TOP-REAL n) No reference.

Corrolary No reference.

Corrolary (for topological spaces and TOP-REAL n) No reference.

2.21 Examples No reference. (Detailed list omitted here.)

2.22 Theorem is SETFAM_1:33 or TOPS_2:6. Counterpart is SETFAM_1:34 or TOPS_2:7.

2.23 Theorem No reference.

2.23 Theorem (for topological spaces) is TOPS_1:4.

Corrolary No reference.

Corrolary (for topological spaces) is TOPS_1:3.

2.24 Theorem
(a) No reference.
(b) No reference.
(c) No reference.
(d) No reference.

2.24 Theorem (for topological spaces)
(a) is TOPS_2:19.
(b) is TOPS_2:22.
(c) is TOPS_2:20.
(d) is TOPS_2:21.

2.25 Examples No reference.

2.26 Definition No reference.

2.26 Definition (for topological spaces) ${\overline {E}}$ is Cl E (PRE_TOPC:def 7), the definition is TOPGEN_1:29 .

2.27 Theorem
(a) No reference.
(b) No reference.
(c) No reference.

2.27 Theorem (for topological spaces)
(a) is clustered in TOPS_1.
(b) is PRE_TOPC:22.
(c) is TOPS_1:5.

2.28 Theorem No reference.

2.29 Remark No reference.

2.30 Theorem given by PRE_TOPC:def 4.

Compact Sets

2.31 Definition is SETFAM_1:def 11.

2.32 Definition No direct reference. compact is defined in TOPMETR:def 5 via the topological definition. See also TOPMETR:16.

2.32 Definition (for topological spaces) is COMPTS_1:def 1. That finite sets are compact is clustered in YELLOW13.

2.33 Theorem No reference.

2.33 Theorem (for topological spaces) is COMPTS_1:3.

2.35 Theorem No reference.

2.35 Theorem (for $T_{2}$ topological spaces) is COMPTS_1:7.

2.35 Theorem No reference.

2.35 Theorem (for topological spaces) is COMPTS_1:8.

Corollary No reference.

Corollary (for topological spaces) No reference.

2.36 Theorem No reference.

2.36 Theorem (for topological spaces) is COMPTS_1:4 with FINSET_1:def 3.

Corollary No reference.

Corollary (for topological spaces) No reference.

2.37 Theorem No reference.

2.38 Theorem is COUSIN:35.

2.39 Theorem No reference. #TODO Find that meet of nested cells is non empty.

2.40 Theorem No reference. #TODO Find that cells are compact.

2.41 Theorem No reference. #TODO Find the Heine-Borel theorem for $R^{k}$, accumulation point variant.

2.42 Theorem No reference. #TODO Find the Weierstrass theorem for $R^{k}$, accumulation point variant.

2.43 Theorem No reference. #TODO Find that nonempty perfect subsets of $R^{k}$ are uncountable.

Corollary No reference, although $R$ being uncountable was discussed in commentary to Theorem 2.14. #TODO Real intervals are uncountable.

2.44 The Cantor set see CANTOR_1. It seems the definition of the_Cantor_set (CANTOR_1:def 5) isn't designed to be a subset of the reals.

Connected Sets

2.45 Definition No reference.

2.45 Definition (for topological spaces) is CONNSP_1:def 1 and CONNSP_1:def 3.

2.46 Remark is CONNSP_1:1. An example quite similar to the one given in the Book is given by BORSUK_4:17.

2.47 Theorem
First two clusterings. pathwise_connected -> connected in BORSUK_2, interval -> pathwise_connected in TOPALG_2. Now an interval has the described properties (XXREAL_2:80) and the given properties describe an interval (XXREAL_2:84). Note difference between XXREAL_2:def 12 and TOPALG_2:def 3.

Exercises

1. is XBOOLE_1:2.
2. Algebraic numbers are given through ALGNUM_1:def 2 and ALGNUM_1:def 4. #TODO Find that the set of algebraic numbers is countable.
3. Existence of liouville (LIOUVIL1:def 5) numbers is clustered in LIOUVIL1. transcendental is introduced as antonym in ALGNUM_1, and liouville numbers are clustered as transcendential in LIOUVIL2.
4. No reference. #TODO Find that irrational numbers have cardinality of continuum.
5. No reference.
6. No reference for metric spaces, since no reference for $E'$ there. If the topological space is $T_{1}$, $E'$ is closed (clustered in TOPGEN_1), $E''\subset E'$ (TOPGEN_1:32) and ${\overline {E'}}=E'$ (TOPGEN_1:33). No reference for $E'={\overline {E}}'$ or example of $E'\neq E''$.
7. No reference for metric spaces. For topological spaces, no reference for finite version (except PRE_TOPC:20), infinite version is TDLAT_2:15.
8. No reference. 9. No refence for metric spaces. For topological spaces, $E^{\circ }$ is Int E (TOPS_1:def 1), see above.
9(a) $E^{\circ }$ open is clustered in TOPS_1.
9(b) is TOPS_1:23.
9(c) is TOPS_1:24.
9(d) is TOPS_1:def 1.
9(e) is supercondensed (ISOMICHI:def 1).
9(f) is subcondensed (ISOMICHI:def 2).
10. is METRIC_1:def 10/11. No reference for open/closed/compact sets.
11. No reference.
12. No reference.
13. No reference.
14. No reference.
15. No reference.
16. No reference.
17. No reference.
18. No reference.
19. No reference for metric spaces. For topological spaces:
19(a) is CONNSP_1:2.
19(b) if $A\cup B$ is the whole space, CONNSP_1:3.
19(c) No reference.
19(d) No reference.
20. No reference.
21(a) No reference.
21(b) No reference.
21(c) No reference.
21(d) No reference.
22. No reference for metric spaces. separable is defined by TOPGEN_1:def 12 and TOPGEN_1:def 13. Separability of $R^{k}$ is given by a series of clusters. TOP-REAL k is clustered second-countable (WAYBEL23:def 6) in MFOLD_0. second-countable -> Lindelof (METRIZTS:def 2) in METRIZTS. Lindelof -> separable in METRIZTS if the topological space is metrizable. No reference for TOP-SPACE k being metrizable (PCOMPS_1:def 8).
23. No reference for metric spaces. Basis of a topological space is defined in CANTOR_1. No reference for the statement. #TODO Find that every separable metric space has countable base.
24. No reference.
25. No reference.
26. No reference.
27. No reference for metric spaces. Condensation points of topological spaces are defined in TOPGEN_4:def 9. The set of condensation points is defined in TOPGEN_4:def 10. No reference for statement.
28. No reference.
29. No reference.
30. No reference.

Convergent Sequences

3.1 Definition
A sequence $S$ of metric space $X$ is a sequence of X (STRUCT_0). $S$ can be convergent (TBSP_1:def 2) and $S$ converges to $x$ means S is_convergent_in_metrspace_to x (METRIC_6:def 2), in which case we may also write lim S = x (TBSP_1:def 3, METRIC_6:12). The range of any relation $R$ is initially defined in XTUPLE_0:def 13 and the synonym rng R is given in RELAT_1. $S$ is bounded (METRIC_6:def 4) if its range is bounded (TBSP_1:def 7, METRIC_6:def 3).

3.1 Definition (for complex and real numbers)
Complex_Sequence is defined in COMSEQ_1, Real_Sequence in SEQ_1. Convergence is COMSEQ_2:def 5 and SEQ_2:def 6, boundedness is COMSEQ_2:def 3/4. Limes is COMSEQ_2:def 6 for complex and SEQ_2:def 7 for real numbers. No reference for examples.

3.1 Definition (for real vectors)
Real_Sequence of N is defined in TOPRNS_1. Convergence is TOPRNS_1:def 8, boundedness is TOPRNS_1:def 7. Limes is TOPRNS_1:def 9.

3.2 Theorem
(a) No reference.
(b) Given by the uniqueness property of the different limes definitions.
(c) No reference for metric spaces. Clustered in COMSEQ_2 for complex and real sequences. Given for real vector sequences by TOPRNS_1:44.
(d) No reference.

3.3 Theorem
(a) is COMSEQ_2:14 and SEQ_2:6 (operation defined in VALUED_1:def 1).
(b) multiplication is COMSEQ_2:18 and SEQ_2:8 (operation defined in VALUED_1:def 5), no reference for addition (operation defined in VALUED_1:def 2).
(c) is COMSEQ_2:30 and SEQ_2:15 (operation defined in VALUED_1:def 4).
(d) is COMSEQ_2:35 and SEQ_2:22 (operation defined in VALUED_1:def 7).

3.4 Theorem
(a) No reference. #TODO Find reference that $x$ is convergent if each $x_{k}$ is convergent
(b) first one is TOPRNS_1:36, no reference for the other two.

Subsequences

3.5 Definition
subsequence is defined in VALUED_0:def 17. The first direction of the remark is given by METRIC_6:24 for metric spaces, SEQ_4:16 for real sequences, no reference for complex sequences, real vector sequences. The other direction has no reference.

3.6 Theorem
No reference for metric spaces or real vector sequences; COMSEQ_3:50 for complex and SEQ_4:40 for real sequences.

3.7 Theorem No reference.

Cauchy Sequences

3.8 Definition
TBSP_1:def 4 for metric spaces, no reference else.

3.9 Definition
TBSP_1:def 8 for subsets of metric spaces, MEASURE5:def 6 for sets of (extended) real numbers, no reference else. No reference for the remark.

3.10 Theorem No references.

3.11 Theorem
(a) TBSP_1:5 for metric spaces, implied by SEQ_4:41 for real sequences, no references else. (b) TBSP_1:8 in combination with TBSP_1:def 5 for metric spaces, again implied by SEQ_4:41 for real sequences, no references else. (c) No reference.

3.12 Definition is TBSP_1:def 5. No reference for remark.

3.13 Definition
Monotonically increasing is non-decreasing (SEQM_3:def 8), monotonically decreasing is non-increasing (SEQM_3:def 9). Monotonic is monotone (SEQM_3:def 5).

3.14 Theorem is SEQ_2:13 and SEQ_4:36 (both clustered in the respective article).

Upper And Lower Limits

3.15 Definition
$s_{n}\rightarrow +\infty$ means s is non bounded_above (SEQ_2:def 1). $s_{n}\rightarrow -\infty$ means s is non bounded_below (SEQ_2:def 2). For extended real sequences (defined in MESFUNC5) the variants convergent_to_+/-infty (MESFUNC5:def 9/10) exist.

3.16 Definition
The definition in the Book has no reference. However, lim_sup/inf are defined in RINFSUP1:def 6/7 and RINFSUP2:def 8/9 respectively. The first variant maps real sequences to reals, therefore excluding $\pm \infty$, the second one maps extended real sequences to extended reals, thereby allowing $\pm \infty$. The identification of the variants for bounded sequences is given by RINFSUP2:9/10.

3.17 Theorem
(a) No reference, except maybe in the case of $\pm \infty$ where it holds by definition.
(b) Implicitly given by RINFSUP1:82/84.
The uniquess property are given again in the definition of the functors.

3.18 Examples
(a) No reference.
(b) No reference.
(c) Given by RINFSUP1:88/89 or RINFSUP2:40/41.

3.19 Theorem
No direct reference, but can be followed from RINFSUP1:91 ($N=0$) in combination with RINFSUP2:28/29.

Some Special Sequences

Remark is SEQ_2:17 with SEQ_2:18, which is a weaker version of the sandwich lemma SEQ_2:19.

3.20 Theorem
(a) ASYMPT_1:69 is stronger version
(b) is PREPOWER:33 or POWER:23.
(c) No reference.
(d) No reference.
(e) is SERIES_1:3.

Series

3.21 Definition
The sum $\sum _{n=p}^{q}a_{n}$ for $p\leq q$ can be expressed via Sum(a, p, q) (SERIES_1:def 6) if $a$ is a sequence.
However, that notation is used rather seldom in the MML. The usual approach is to have the summands as a tuple (in form of a FinSequence (FINSEQ_1) of real or complex numbers) and use Sum a (RVSUM_1:def 10). The usual operations of sums are defined in RVSUM_1/2, too. If the upper and lower limit are indeed needed, a possible variant would be Sum (a|q/^p) (FINSEQ_1:def 15, RFINSEQ:def 1). Also see NEWTON04:37.
In comparison to that, $s_{n}$ is simply Partial_Sums(s) (SERIES_1:def 1). The series converging means a is summable (SERIES_1:def 2 for real, COMSEQ_3:def 8 for complex), it limes is Sum a (SERIES_1:def 3). (Note that in the paragraph above, a referred to a FinSequence, while in this paragraph, it refers to a Real_sequence, so the Sum functors with a single argument behind it in these both paragraphs are different ones.)
Note that series in Mizar always start with $0$ because they are ManySortedSet of NAT and 0 in NAT. Inconvenient summands, like ${\tfrac {1}{0}}$ in the series of ${\tfrac {1}{n}}$, usually turn out to be 0 in Mizar, or the sequence to be summed is defined to be fitting with this notation just beforehand.

3.22 Theorem is SERIES_1:21.

3.23 Theorem is SERIES_1:4.

3.24 Theorem is SERIES_1:17.

3.25 Theorem
(a) COMSEQ_3:66, weaker version is SERIES_1:19.
(b) No reference.

Series Of Nonnegative Terms

3.26 Theorem
The geometric sequence is defined in PREPOWER:def 1 for real base and in COMSEQ_3:def 1 for complex base. Their sum for $|x|<1$ is given by SERIES_1:24 or COMSEQ_3:64 for $x$ being real or complex respectively. No reference for $|x|\geq 1$.

3.27 Theorem is SERIES_1:31 or COMSEQ_3:72 for real or complex sequences respectively.

3.28 Theorem is SERIES_1:32/33 or COMSEQ_3:73/74 for real or complex sequences respectively.

3.29 Theorem No reference.

The Number $e$

3.30 Definition
$n!$ is defined in NEWTON:def 2. $e$ is number_e (POWER:def 4), $e^{x}$ is exp_R (SIN_COS:def 22). $e=e^{1}$ is given by IRRAT_1:def 7. Then the definition of the Book is given by IRRAT_1:def 5 and IRRAT_1:23.

3.31 Theorem is given by IRRAT_1:def 4 and IRRAT_1:22.

3.32 Theorem is IRRAT_1:41.

The Root And Ratio Tests

3.33 Theorem
(a) is basically SERIES_1:40 or COMSEQ_3:69 for real or complex sequences respectively.
(b) is basically SERIES_1:41 or COMSEQ_3:70 for real or complex sequences respectively.
(c) No reference.

3.34 Theorem
(a) is basically SERIES_1:37 or COMSEQ_3:75 for real or complex sequences respectively.
(a) is basically SERIES_1:39 or COMSEQ_3:76 for real or complex sequences respectively.

3.35 Examples No reference.

3.36 Remark Nothing to formalize.

3.37 Theorem No reference.

Power Series

3.38 Definition No reference.

3.39 Theorem No reference.

3.40 Examples No reference.

Summation By Parts

3.41 Theorem No reference.

3.42 Theorem No reference.

3.43 Theorem is LEIBNIZ1:8.

3.44 Theorem No reference.

Absolute Convergence

$a$ converging absolutely means a is absolutely_summable (SERIES_1:def 4 or COMSEQ_3:def 9).

3.45 Theorem is SERIES_1:35 or COMSEQ_3:63 and clustered in both articles.

3.46 Remark No reference.

Addition And Multiplication Of Series

3.47 Theorem
For real sequences, SERIES_1:7 and SERIES_1:10.
For complex sequences, COMSEQ_3:54 and COMSEQ_3:56.

3.48 Definition No reference. #TODO Find reference for Cauchy product of two series.

3.49 Example No reference.

3.50 Theorem No reference.

3.51 Theorem No reference.

Rearrangements

3.52 Definition
A Permutation of NAT is defined in FUNCT_2, but no reference for rearrangements.

3.53 Example No reference.

3.54 Theorem No reference.

3.55 Theorem No reference.

Exercises

1. clustered in SEQ_2 for real sequences, no reference for complex sequences or converse (which is false).
2. No reference.
3. No reference.
4. No reference.
5. is in RINFSUP1:92 in bounded case, for the other one no reference.
6. No reference.
7. No reference.
8. No reference.
9. No reference.
10. No reference.
11. No reference.
12. No reference.
13. No reference. #TODO Find reference that Cauchy product of two abs conv series is abs conv.
14. No reference.
15. No reference.
16. No reference. #TODO Find reference for convergence towards ${\sqrt {\alpha }}$
17. No reference.
18. No reference.
19. No reference. #TODO Find reference for ternary representation of reals in the Cantor set.
20. No reference.
21. No reference.
22. No reference. #TODO Find reference for Baire's theorem
23. No reference.
24. No reference.
25. No reference.

Limits of Functions

4.1 Definition
For real numbers given by LIMFUNC3:28. Else no reference.

4.2 Theorem
For real numbers lim(f,p) is defined in LIMFUNC3:def 4. Else no reference.

Corollary
Given by the uniqueness property of lim(f,p).

4.3 Definition
$f+g$, $f-g$, $fg$ and $f/g$ are given by VALUED_1:def 1, VALUED_1:def 9, VALUED_1:def 4 and [VALUED_1:def 10 or RFUNCT_1:def 1 (the former maps inverse of 0 to 0, the latter removes these from the domain)] respectively. f is constant is defined in FUNCT_1:def 10, $f=c$ is E --> c (FUNCOP_1:def 2), with clusters in VALUED_0. $f\geq g$ is defined in COUSIN2:def 3. Addition of functions yielding complex vectors is given by INTEGR15:def 9 and VALUED_2:def 45, component-wise multiplication by VALUED_2:def 47. The clustering for the vectors is given in TOPREALC. Scalar multiplication is given by VALUED_1:def 5, with correct clustering in the same file.

4.4 Theorem
For reals:
(a) is LIMFUNC3:33.
(b) is LIMFUNC3:38.
(c) is LIMFUNC3:39.
Else no references.

Remark No reference.

Continuous Functions

4.5 Definition
Continuity of a function between topological spaces in a point is defined in TMAP_1:def 2, on the whole domain in TMAP_1:44 (see also PRE_TOPC:def 6). No reference for metric spaces.
For real functions given by FCONT_1:3 in a point and by FCONT_1:def 2 for whole domain.
For complex functions given by CFCONT_1:32 in a point and by FCONT_1:def 2 for a domain.
For real vectors by NFCONT_1:7 (see also PDIFF_7:def 6) in a point and by NFCONT_1:def 7 for a domain.

4.6 Theorem
No direct reference, in spirit given by the referred theorems under 4.5 in combination with the definitions using sequences (see FCONT_1:def 1, CFCONT_1:def 1 and NFCONT_1:def 5).

4.7 Theorem
For topological spaces given by TMAP_1:47 (pointwise) and TOPS_2:46 (whole domain).
For real functions given by FCONT_1:12 (pointwise) and clustered there for whole domain.
Else no reference.

4.8 Theorem
For topological spaces given by TOPS_2:43. For real functions and real vectors only given in neighborhood variant (FCONT_1:5 and NFCONT_1:9 (the latter only pointwise)). No reference else.

Corollary is given by original definition PRE_TOPC:def 6 for topological spaces, else no reference.

4.9 Theorem
For real functions given by FCONT_1:7 and FCONT_1:11 (pointwise) and clustered there, except for $f/g$ (FCONT_1:24) (whole domain).
For complex functions given by CFCONT_1:33 and CFCONT_1:37 (pointwise) and by CFCONT_1:43 and CFCONT_1:49 on domain.

4.10 Theorem
(a) Only special case where the metric space is $R$ in NFCONT_4:43.
(b) Only addition in NFCONT_1:15.

4.11 Examples
The projections are defined in PDIFF_1:def 1. No reference for the continuity of general polynoms or rational functions. $|x|$ is continuous by NFCONT_1:17 (pointwise) and NFCONT_1:28 (domain).

4.12 Remark Nothing to formalize.

Continuity and Compactness

4.13 Definition
For real functions given by RFUNCT_1:72, for complex functions given by SEQ_2:def 5. For functions into $R^{k}$ implicitly given by INTEGR19:14 (the left bounded is from INTEGR15:def 12) which basically uses the maximum norm (compare NFCONT_4:def 2). No direct reference for the Euclidean norm.

4.14 Theorem
For topological spaces more generally given by COMPTS_1:15 or WEIERSTR:8. For real functions given by FCONT_1:29, for complex functions by CFCONT_1:52. For real vectors given by NFCONT_1:32.

4.15 Theorem
In PSCOMP_1 clustered via use of pseudocompactness of topological spaces (PSCOMP_1:def 4). No reference for metric spaces. For real domain directly given by INTEGRA5:10.

4.16 Theorem
In PSCOMP_1 clustered via use of pseudocompactness of topological spaces (PSCOMP_1:def 4), again. No reference for metric spaces as well. For real domain directly given by FCONT_1:30.

4.17 Theorem No reference. Next best variant for real functions would be FCONT_3:22.

4.18 Definition
For metric spaces given by UNIFORM1:def 1. For real functions given by FCONT_2:def 1. For vectors given by NFCONT_2:def 1, see also INTEGR20:def 1 and the definitions in NCFCONT2.
That uniform continuous functions are continuous is given by UNIFORM1:5 for metric spaces (indirectly), by FCONT_2:9 for real functions and by NFCONT_2:7 for vectors.

4.19 Theorem
For metric spaces indirectly given by UNIFORM1:7. For real functions given by FCONT_2:11, for vectors given by NFCONT_2:10.

4.20 Theorem
(a) No reference.
(b) No reference.
(c) No reference.

4.21 Example
$f(2\pi t)$ as a function defined on the real line is given by CircleMap in TOPREALB:def 11. The continuity of that function as well as its surjectivness and injectiveness (the latter only if restricted to a half-open interval of length 1) is clustered there as well. No reference for the inverse explicitly not being continuous.

Continuity and Connectedness

4.22 Theorem
Given more generally for topological spaces by TOPS_2:61. No reference specifically for real functions.

4.23 Theorem
TOPREAL5:8, generalized version is TOPREAL5:5. No reference for version with simple real functions. #TODO Find simple version of intermediate value theorem.

4.24 Example No reference.

Discontinuities

4.25 Definition
$f(x\pm )$ is lim_right/left(f,x) (LIMFUNC2:def 8/7). The "It is clear" is LIMFUNC3:29/30.

4.26 Definition
No direct reference, although the properties are indirectly given: $f$ having a discontinuity of the first kind at $x$ means not f is_convergent_in x & f is_left_convergent_in x & f is_right_convergent_in x; $f$ having a discontinuity of the second kind at $x$ means not f is_left_convergent_in x or not f is_right_convergent_in x.

4.27 Examples
(a) $f$ is given by (REAL --> 1) - chi(RAT,REAL) (see FUNCOP_1:def 2 and FUNCT_3:def 3). No reference for the discontinuity property.
(b) $f$ is given by (id REAL)*((REAL --> 1) - chi(RAT,REAL)) (see additionally RELAT_1:def 10 and the functional properties in FUNCT_1). No reference for the discontinuity property.
(c) No reference.
(d) $f$ is given by sin((id REAL)^) +* (0 .--> 0) (see SIN_COS:def 16, RFUNCT_1:def 2, FUNCT_4:def 1 and FUNCOP_1:def 9). No reference for the discontinuity property.

Monotonic Functions

4.28 Definition
Monotonically increasing/decreasing is non-decreasing/increasing (VALUED_0:def 15/16). The monotone property is in RFUNCT_2:def 5.

4.29 Theorem No reference, although FCONT_3 is full of related result.

Corollary No reference.

4.30 Theorem No reference. #TODO Find proof that number of discontinuities of a monotone function are at most countable.

4.31 Remark No reference.

Infinite Limits and Limits at Infinity

4.32 Definition No reference, although open intervals were defined in Mizar with infinity in mind.

4.33 Definition
Limits at infinity are explicitly formalized as lim_in+infty f and lim_in-infty f (LIMFUNC1:def 12/13).

4.34 Theorem
uniqueness is given again by property of definitions LIMFUNC1:def 12/13. $f+g$, $fg$ and $f/g$ are given by LIMFUNC1:82/91, LIMFUNC1:87/96 and LIMFUNC1:88/97 respectively.

Exercises

1. No reference.
2. No reference, including no counterexample for the backwards direction. #TODO Show that $f({\overline {E}})\subset {\overline {f(E)}}$.
3. $Z(f)$ is usually referred to as f"{0} (FUNCT_1:def 7). No direct reference, but pretty obvious even by Mizar standard. Because of PRE_TOPC:def 6 we only need to show that {0} is closed in R^1 and we get that from clustering R^1 -> T_2 -> T_1 (TOPREAL6 and PRE_TOPC) and URYSOHN1:19.
4. No reference. #TODO Proof that images of dense sets under continuous functions are dense and that continuous functions are determined by their dense subsets.
5. No reference. Basically the simple case of 4 for real functions.
6. No reference. Since functions are relations in Mizar, $f$ consists of elements of the form [x,f.x]. However, for a proper embedding into TOP-REAL 2 one would need the set of all <*x,f.x*>.
7. $g$ is referred to as f|E (RELAT_1:def 11). No reference for the exercise.
8. No reference.
9. No reference.
10. No reference.
11. No reference.
12. No reference. #TODO Compositions of uniformly continuous functions are uniformly continuous.
13. No reference.
14. No reference. #TODO Existence of fixpoint for continuous $f:[0,1]\rightarrow [0,1]$.
15. open is defined in T_0TOPSP:def 2. No reference for exercise.
16. $[x]$ is [\x/] (INT_1:def 6), $(x)$ is frac x (INT_1:def 8). No reference for exercise.
17. No reference.
18. No reference.
19. No reference.
20. $\rho _{E}(x)$ is given by dist(x,E) (SEQ_4:def 17 (complex vectors), JORDAN1K:def 2 (real vectors)). No references for exercises.
20.(a) No reference, but see SEQ_4:116 and JORDAN1K:45.
20.(b) No reference. 21. No reference.
22. No reference.
23. No reference. For convexity see CONVFUN1:4.
24. No reference.
25. No reference.
26. No reference.

The Derivative of a Real Function

5.1 Definition
Mizar does not introduce differentiation via $\phi (t)$ as Rudin does, but works directly with linear and rest functions (see FDIFF_1:def 2/3). There is no reference associating the Mizar differentiation with the notation of LIMFUNC3, but there are FDIFF_1:12 and FDIFF_2:49. (On a side note, Mizar differentiation is not restricted to intervals $[a,b]$.)
$f$ is differentiable at $x$ means f is_differentiable_in x (FDIFF_1:def 4), $f'(x)$ is diff(f,x) (FDIFF_1:def 5). $f$ is differentiable on $E$ means f is_differentiable_on E (FDIFF_1:def 6), $f'$ is f`|E (FDIFF_1:def 7). See also FDIFF_1:def 8 and POLYDIFF:def 1.
One-side differentiation is covered in FDIFF_3.

5.2 Theorem is FDIFF_1:24/25

5.3 Theorem
(a) is FDIFF_1:13/18 or POLYDIFF:14.
(b) is FDIFF_1:16/21 or POLYDIFF:16.
(c) is FDIFF_2:14/21.

5.4 Examples
$c'=0$ for constant $c$ is FDIFF_1:11/22, see also POLYDIFF:11.
$x'=1$ is FDIFF_1:17, see also POLYDIFF:12, and more general $(ax+b)'=a$ is FDIFF_1:23.
Differentiation of polynomials is given by POLYDIFF:def 5/6 and POLYDIFF:61. The notations seems a little bit sophisticated because polynomials have quite some structure behind them in Mizar, see PRE_POLY and the POLYNOM series.

5.5 Theorem is FDIFF_2:23.

5.6 Examples
(a) is FDIFF_5:7.
(b) is FDIFF_5:17, although $f'(0)$ has been explicitly excluded, no reference for that.

Mean Value Theorems

5.7 Definition No reference.

5.8 Theorem No reference, although the statement is basically proven within the proof of ROLLE:1. #TODO Explicit reference that local extrema of differentiable functions have derivation 0.

5.9 Theorem is ROLLE:5.

5.10 Theorem is ROLLE:3.

5.11 Theorem
(a) is ROLLE:11 or FDIFF_2:31.
(b) is ROLLE:7.
(c) is ROLLE:12 or FDIFF_2:32.

The Continuity of Derivatives

5.12 Theorem No reference. #TODO $f'(a)<\lambda <f'(b)$ implies the existence of an $x$ such that $f'(x)=\lambda$.

Corollary No reference.

L'Hospital's Rule

5.13 Theorem in L_HOSPIT, especially L_HOSPIT:10.

Derivatives of Higher Order

5.14 Definition
$f^{(n)}$ is diff(f,E).n (TAYLOR_1:def 5, see also TAYLOR_1:def 6), where $E$ is the domain on which $f^{(n)}$ is defined.

Taylor's Theorem

5.15 Theorem
Set $c=\alpha$ and $d=\beta$, then $P(t)$ is Partial_Sums(Taylor(f,E,c,d)).(n-'1) (see SERIES_1:def 1 and TAYLOR_1:def 7), where $E$ is the domain on which $f^{(n)}$ is defined. The theorem is TAYLOR_1:27 with $n+1$ instead of $n$.

Differentiation of vector-valued Functions

5.16 Remark (about complex-valued functions)
Differentiation of functions from a subset of the reals to the complex are not formalized in Mizar, but definitions for complex differentiation are given by CFDIFF_1:def 6-9 and CFDIFF_1:def 12, see also CFDIFF_1:22. Continuity of differentiable complex functions is given by CFDIFF_1:34/35. The differentiation rules $f+g$ and $fg$ are given by CFDIFF_1:23/28, CFDIFF_1:26/31 respectively. No reference for $f/g$.

5.16 Remark (about normed spaces)
In NDIFF_1 differentiation is defined between normed linear spaces (see NDIFF_1:def 6-9), i.e. the domain doesn't need to be a subset of the real numbers. No reference for differentiability iff the components are differentiable. See also PDIFF_1.
That differentiability implies continuity is given by NDIFF_1:44/45.
$f+g$ is given by NDIFF_1:35/39. No reference for inner product.

5.16 Remark (about vector-valued functions)
For definitions see NDIFF_3:def 3-7, see also NDIFF_3:13. No reference for differentiability iff the components are differentiable. See also NDIFF_4.
That differentiability implies continuity is given by NDIFF_3:22/23.
$f+g$ is given by NDIFF_3:14/17. No reference for inner product.

5.17 Examples No reference. $e^{z}$ is defined in SIN_COS:def 14, $e^{ix}$ is given by SIN_COS:25.

5.18 Examples No reference.

5.19 Theorem No reference.

Exercises

1. is FDIFF_2:25.
2. is FDIFF_2:37/38 or FDIFF_2:45.
3. No reference.
4. No reference.
5. No reference.
6. No reference.
7. see L_HOSPIT:10.
8. No reference.
9. No reference.
10. No reference.
11. No reference.
12. No reference.
13. No reference.
14. No reference.
15. No reference.
16. No reference.
17. No reference.
18. No reference.
19. No reference.
20. No reference.
21. No reference.
22. No reference.
23. No reference.
24. No reference.
25. No reference.
26. No reference. #TODO Find reference that $|f(x)|\leq A|f'(x)|$ implies $f=0$.
27. No reference. #TODO Find reference for initial value problem.
28. No reference. #TODO Find reference for initial value problem.
29. No reference. In Mizar the Riemann-Stieltjes integral wasn't formalized until recently, so this chapter will primarily deal with that variant. Everything about the Riemann-Stieltjes integral in Mizar at the time of writing is in INTEGR22 and INTEGR23.

Definition and Existence of the Integral

6.1 Definition
A partition is described by a Division (INTEGRA1:def 2), leaving $x_{0}$ out and changing $\leq$ to $<$. The intervals can be accessed via divset(P,i) (INTEGRA1:def 4), therefore $\Delta x_{i}$ is given by vol divset(P,i) (INTEGRA1:def 5).
$U(P,f)$ is upper_sum(f,P) (INTEGRA1:def 8), $L(P,f)$ is lower_sum(f,P) (INTEGRA1:def 9).
$\textstyle {\overline {\int }}_{a}^{b}f\,dx$ is upper_integral(f) (INTEGRA1:def 14), $\textstyle {\underline {\int }}_{a}^{b}f\,dx$ is lower_integral(f) (INTEGRA1:def 15).
$f$ being integrable is in INTEGRA1:def 16 (see also INTEGRA5:def 1), $\textstyle {\int }_{a}^{b}f\,dx$ is integral(f) (INTEGRA1:def 17, see also INTEGRA5:def 4 for explicit integration bounds and INTEGRA7:def 2 for indefinite integral).
The inequalities are given by INTEGRA1:25,28,27.

6.2 Definition in INTEGR22.

6.3 Definition
Refinement is INTEGRA1:def 18. No reference for definition of common refinement, but it is given by INTEGRA1:47 and more precise by INTEGRA3:21.

6.4 Theorem is INTEGRA1:41/40.

6.5 Theorem is INTEGRA1:49.

6.6 Theorem is implicitly given by INTEGRA4:12.

6.7 Theorem No reference.

6.8 Theorem is INTEGRA5:11, for Riemann-Stieltjes INTEGR23:21.

6.9 Theorem is INTEGRA5:16.

6.10 Theorem No reference.

6.11 Theorem No reference. #TODO Reference that if $f$ is bounded and integrable and $\phi$ is continuous, then $\phi \circ f$ is integrable.

Properties of the Integral

6.12 Theorem
(a) is INTEGRA1:57 or INTEGRA6:11 and INTEGRA2:31 or INTEGRA6:9.
(b) is INTEGRA2:34.
(c) is INTEGRA6:17. No reference for something like $\textstyle \int _{A\cup B}f\,dx=\int _{A}f\,dx+\int _{B}f\,dx$ with $A\cap B=\emptyset$.
(d) No direct reference, but 6.13(b) improves the bound anyway.
(d) No reference.

6.13 Theorem
(a) is INTEGRA4:29.
(b) is INTEGRA4:23 or INTEGRA6:7/8.

6.14 Definition
$I$ equals chi(REALPLUS,REAL) (FUNCT_3:def 3, MUSIC_S1:def 2).

6.15 Theorem No reference.

6.16 Theorem No reference.

6.17 Theorem No reference. #TODO Relation between the Riemann and the Riemann-Stieltjes integral.

6.18 Remark No reference.

6.19 Theorem (change of variable) No reference. #TODO Find reference!

Integration and Differentiation

6.20 Theorem
INTEGRA6:28/29, but no reference for the continuity of $F$ if $f$ is only integrable.

6.21 The fundamental theorem of calculus is INTEGRA7:10.

6.22 Theorem (integration by parts) is INTEGRA5:21 or INTEGRA7:21/22.

Integration of vector-valued Functions

6.23 Definition Given by INTEGR15:def 13/14 and INTEGR15:def 16-18. Theorem 6.12 (a) translates to INTEGR15:17/18. Theorem 6.12 (c) translates to INTEGR19:8. No reference for a translation of Theorem 6.12 (e) or Theorem 6.17, since we're still looking at Riemann integrals only.

6.24 Theorem
No direct reference, but with continuity given by INTEGR19:55/56.

6.25 Theorem is INTEGR19:20/21.

Rectifiable Curves

6.26 Definition
More generally, $\gamma$ being a parametrized-curve is defined in TOPALG_6:def 4, no reference for closed curves there. For simple closed curves in $R^{2}$ see the attribute being_simple_closed_curve (TOPREAL2:def 1). In pursuing the proof of the Jordan Curve Theorem a lot of articles have been written dealing with that attribute, in contrast to parametrized-curve. Also see INTEGR1C:def 3 for a formalization of ${\mathcal {C}}^{1}$-curves using another approach.
No reference for $\Lambda (\gamma )$ or rectifiable.

6.27 Theorem No reference.

Exercises

1. No reference.
2. No reference.
3. No reference.
4. No reference.
5. No reference.
6. No reference.
7. No reference.
8. See INTEGR10 for the definitions. No reference for exercise.
9. No reference.
10. No reference.
11. No reference.
12. No reference.
13. No reference.
14. No reference.
15. No reference.
16. No reference.
17. No reference.
18. No reference.
19. No reference. Note that sequences of functions can be seen as sequences over a normed space, which will mostly be left untouched in this chapter.

Discussion of main problem

7.1 Definition
Let $F$ denote $\{f_{n}\}$. $F$ being pointwise convergent is described by F is_point_conv_on E (SEQFUNC:20, see also SEQFUNC:def 10). Then $\lim _{n\to \infty }f_{n}$ is given by lim(F,E) (SEQFUNC:def 13). No reference for series.

7.2 Example No reference.

7.3 Example No reference.

7.4 Example No reference.

7.5 Example No reference.

7.6 Example No reference.

Uniform Convergence

7.7 Definition
$F$ being uniformly convergent on $E$ is F is_unif_conv_on E (SEQFUNC:def 12) or F is_uniformly_convergent_to f (MESFUN10:def 2. That uniform convergence implies pointwise convergence is SEQFUNC:22 or MESFUN10:20. No reference for function series.

7.8 Theorem
No reference.

7.9 Theorem
No reference.

7.10 Theorem
No reference.

Uniform Convergence and Continuity

7.11 Theorem No direct reference, but implicitly given in proof of TIETZE:20.

7.12 Theorem is TIETZE:20.

7.13 Theorem No reference.

7.14 Definition
No reference.

7.15 Theorem No reference.

Uniform Convergence and Integration

7.16 Theorem is INTEGRA7:31 or MESFUN10:21.

Corollary No reference.

Uniform Convergence and Differentiation

7.17 Theorem No reference. #TODO show that $f'(x)=\lim _{n\to \infty }f_{n}(x)$

7.18 Theorem No reference. #TODO existence of continuous nowhere differentiable function

Equicontinuous Families of Functions

7.19 Definition
No reference for pointwise bounded, but for F is uniformly_bounded (MESFUN10:def 1).

7.20 Example No reference.

7.21 Example No reference.

7.22 Definition No reference.

7.23 Theorem No reference.

7.24 Theorem No reference.

7.25 Theorem No reference.

The Stone-Weierstrass Theorem

7.26 Theorem No reference #TODO the Stone-Weierstrass theorem

7.27 Corollary No reference.

7.28 Definition
The algebra of complex functions on a domain $E$ is CAlgebra(E) (CFUNCDOM:def 8), the real analogon of that is RAlgebra(E) (FUNCSDOM:def 9). A general algebra structure is found in POLYALG (not to be confused with the universal algebra from UNIALG_1). Subalgebras for complex algebras are defined in CC0SP1:def 1, for real algebras in C0SP1:def 9. No reference for uniformly closed or uniformly closure.

7.29 Theorem No reference.

7.30 Definition No reference.

7.31 Theorem No reference.

7.32 Theorem No reference.

7.33 Theorem No reference.

Exercises

1. No reference.
2. No reference.
3. No reference.
4. No reference.
5. No reference.
6. No reference.
7. No reference.
8. No reference.
9. No reference.
10. No reference.
11. No reference.
12. No reference.
13. No reference.
14. No reference.
15. No reference.
16. No reference.
17. No reference.
18. No reference.
19. No reference.
20. No reference.
21. No reference.
22. No reference.
23. No reference.
24. No reference.
25. No reference.
26. No reference.

Power Series

8.1 Theorem No reference.

Corollary No reference.

8.2 Theorem No reference.

8.3 Theorem No reference, but see DBLSEQ_1/2.

8.4 Theorem No reference.

8.5 Theorem No reference.

The Exponential and Logarithmic Functions

The series expansion of the exponential function is given via SIN_COS:def 5 and TAYLOR_2:16.

8.6 Theorem
(a) Continuity is clustered in SIN_COS, differentiability is given by TAYLOR_1:16.
(b) TAYLOR_1:16, SIN_COS:65/66 or INTEGRA8:32.
(c) Monotonicity implicitly given by TAYLOR_1:16, positivity implicitly there too, but also explicitly by SIN_COS:52/53.
(d) SIN_COS:23 or SIN_COS:46. SIN_COS:50 or SIN_COS2:12 for reals only. $e^{0}=1$ is given by SIN_COS:51 or SIN_COS2:13.
(e) No direct reference for the limits but see TAYLOR_1:16, where they are implicitly given.
(f) Implicitly given by ASYMPT_2:25 (in combination with ASYMPT_0:15-17 and ASYMPT_2:def 1).

$E(L(y))=y$ is given by POWER:def 3 or TAYLOR_1:14/15, $L(E(x))=x$ is given by TAYLOR_1:12/13 or MOEBIUS3:16. $L'(y)={\tfrac {1}{y}}$ is given by FDIFF_4:1 or TAYLOR_1:18. The addition formula for logarithms is given by POWER:53 or MOEBIUS3:19. The limits are again only indirectly given by TAYLOR_1:18. $x^{\alpha }=e^{\alpha \log x}$ is given by FDIFF_6:1. No reference for $\log x$ being lower than any positive power of $x$.

The Trigonometric Functions

$C(x)$ and $S(x)$ are defined in SIN_COS3:def 2 and SIN_COS3:def 1 respectively. $E(ix)=C(x)+iS(x)$ is given by SIN_COS3:36 (or more general by SIN_COS3:19). $|E(ix)|=1$ is given by SIN_COS:27. No reference for derivates in complex case, but in real case given by SIN_COS:63/64. $\pi$ in Mizar is defined as the unique $x\in (0,4)$ such that $\tan {\tfrac {\pi }{4}}=1$ (SIN_COS:def 28). $\cos(2\pi )=0$ is given by SIN_COS:76/77, that $\pi$ is the smallest positive number with that property is given by SIN_COS:80/81. The rest of the properties is given by SIN_COS3:27-33.

8.7 Theorem
(a) No direct reference, only implicitly by SIN_COS3:27.
(b) SIN_COS3:35/34 (complex) or SIN_COS2:11/10 (real).
(c) No reference.
(d) No reference.

No reference for the circumference of the unit circle, but see TOPREALB:def 11 for a parametrization of it.

The Algebraic Completeness of the Complex Field

8.8 Theorem is POLYNOM5:74.

Fourier Series

8.9 Definition No reference.

8.10 Definition No reference.

8.11 Theorem No reference.

8.12 Theorem No reference.

8.13 Trigonometric series No reference.

8.14 Theorem No reference.

Corollary No reference.

8.15 Theorem No reference.

8.16 Theorem No reference.

The Gamma Function

8.17 Definition No reference.

8.18 Theorem No reference.

8.19 Theorem No reference.

8.20 Theorem No reference.

8.21 Some consequences No reference.

8.22 Stirling's formula No reference.

Exercises

1. No reference.
2. No reference.
3. No reference.
4.(a) No reference.
4.(b) No reference.
4.(c) No reference.
4.(d) No reference, except for $x=1$ in IRRAT_1:22 (see IRRAT_1:def 4).
5. No reference.
6. No reference.
7. No reference.
8. No reference.
9. No reference.
10. No reference.
11. No reference.
12. No reference.
13. No reference, but the result is BASEL_2:32 (see also BASEL_1:31).
14. No reference.
15. No reference.
16. No reference.
17. No reference.
18. No reference.
19. No reference.
20. No reference.
21. No reference.
22. No reference.
23. No reference.
24. No reference.
25. No reference.
26. No reference.
27. No reference.
28. No reference.
29. is BROUWER:15.
30. No reference.
31. No reference.

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. Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Integration of Differential Forms Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/The Lebesgue Theory Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Bibliography