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

This is the print version of Mizar Commentary on Walter Rudin's Principles of Mathematical AnalysisYou won't see this message or any elements not part of the book's content when you print or preview this page. |

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

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**

is `x in A` from `HIDDEN` (and therefore always present without reference). 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`.

is `A c= B` (`TARSKI:def 3`), there is no reference for . being a `proper` Subset of (`SUBSET_1:def 6`) can also be written as `A c< B` (`XBOOLE_0:def 8`). is given by the reflexivity property of `c=` in `TARSKI:def 3`.

is redefined in `XBOOLE_0:def 10`, is generally introduced as an antonym in `HIDDEN`.

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

## Ordered Sets[edit | edit source]

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 and (`ZFMISC_1:def 2`). Many properties of relations are introduced in `RELAT_2`.

**1.5 Definition** The order on 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 is denoted by `a <= b` (`ORDERS_2:def 5`) and 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 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)**

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

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 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. is finally done in `ARITHM:1`, which should be included by `requirements`, not by `theorems`.

(A5) is `XCMPLX_0:def 6`.

(M4) , like all other numerals in Mizar, is defined implicitly. `CARD_1:49` states , with the irreflexivity property built into `in` and `TARSKI:def 1` one can show that whenever needed, no direct reference. 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) is `ALGSTR_0:def 14`, is `ALGSTR_0:def 43`. Functors in Mizar are left-associative, hence `x+y+z=(x+y)+z` is built in, same for multiplication. is `x |^ n` (`GROUP_1:def 9`), , are given by `GROUP_1:27`, `GROUP_1:28`. is `n * x` (`GROUP_1A:def 8`), , are given by `GROUP_1A:26`, `GROUP_1A:26`.

(a) (with complex numbers) is `XCMPLX_0:def 8`, 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). , and are in `XCMPLX_1` and can be used without a problem. is `SQUARE_1:def 1`, is defined in `NEWTON:def 1` (for natural ), , , 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 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`. is built into the appropiate `requirements`.

(e) is `XREAL_1:88` and `XREAL_1:122`.

## The Real Field[edit | edit source]

**1.19 Theorem** Existence of 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 is written as `n -Root x`. Also written as `n -root x` (`POWER:def 1`). 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 .

## The Extended Real Number System[edit | edit source]

**1.23 Definition**

/ are defined in `XXREAL_0:def 2/3`. 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 / 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 are set to 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[edit | edit source]

**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 isn't . 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 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 , 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`, is `<i>`.

**1.28 Theorem** is `COMPLEX1:18`.

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

'*1.30 Definition*

is `z*'` (`COMPLEX1:def 11`).

/ 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**

is `|.z.|` (`COMPLEX1:def 12`, see also `SQUARE_1:def 2`).

is given as a reduction in `COMPLEX1`, 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 , the notion of tuples is needed. This is done in `FINSEQ_1`, defining tuples as functions with domain . 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 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[edit | edit source]

**1.36 Definitions**

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 is `|( x,y )|` (`RVSUM_1:def 16`), the norm is `|. x .|` (`EUCLID:def 5`, see also `RVSUM_1:def 8`), their relation is `EUCLID_2:37`.

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, is `Euclid k` (`EUCLID:def 7`). As a topological space, it is `TOP-REAL k` (`EUCLID:def 8`). 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[edit | edit source]

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

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 . 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 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[edit | edit source]

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` is defined by `FUNCT_1:def 1`. 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 `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**

is `f.:E` (`RELAT_1:def 13`, `FUNCT_1:def 6`), the remark is `RELAT_1:113`. is encoded in `RELSET_1`. Onto is `onto` (`FUNCT_2:def 3`).

is `f"E` (`RELAT_1:def 14`, `FUNCT_1:def 7`). 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 and 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**

is `Seg n` (`FINSEQ_1:def 1`), is `NATPLUS` (`NAT_LAT:def 6`), although it should be mentioned that in Mizar `NAT` (`ORDINAL1:def 11`, synonym introduced in `NUMBERS`) being 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 is finite by `FINSEQ_1:56`. If 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 `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 (but not necessarily a certain range), a `ManySortedSet of X` is a `total X-defined Function` (`PBOOLE`). Then a sequence in Mizar (starting with instead of ) is a `ManySortedSet of NAT`. If it is a sequence of elements of some , 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 of subsets of 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. is `E1 \/ E2` (`XBOOLE_0:def 3`). The intersection of is `meet E` (`SETFAM_1:def 1`). is `E1 /\ E2` (`XBOOLE_0:def 4`). and 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[edit | edit source]

**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, as a metric space is `Euclid n` (`EUCLID:def 7`), is also RealSpace (`METRIC_1:def 13`).

Subsets of 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**

is `].a,b.[` (`XXREAL_1:def 4`), is `[.a,b.]` (`XXREAL_1:def 1`), is `[.a,b.[` (`XXREAL_1:def 2`), is `].a,b.]` (`XXREAL_1:def 3`).

A -cell is `cell(a,b)` (`CHAIN_1:def 6`).

The open/closed ball with center and radius 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) " is a limit point of " 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 , the derivative of , is

`Der E`(

`TOPGEN_1:def 3`), which gives a second characterization via

`TOPGEN_1:17`.

(c) Just like that, " is a isolated point of " 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 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)** 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[edit | edit source]

**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 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 , accumulation point variant.

**2.42 Theorem** No reference. #TODO Find the Weierstrass theorem for , accumulation point variant.

**2.43 Theorem** No reference. #TODO Find that nonempty perfect subsets of are uncountable.

**Corollary** No reference, although 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[edit | edit source]

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

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 there. If the topological space is , is closed (clustered in `TOPGEN_1`), (`TOPGEN_1:32`) and (`TOPGEN_1:33`). No reference for or example of .

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, is `Int E` (`TOPS_1:def 1`), see above.

9(a) 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 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 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[edit | edit source]

**3.1 Definition**

A sequence of metric space is a `sequence of X` (`STRUCT_0`). can be `convergent` (`TBSP_1:def 2`) and converges to 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 is initially defined in `XTUPLE_0:def 13` and the synonym `rng R` is given in `RELAT_1`. 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 is convergent if each is convergent

(b) first one is `TOPRNS_1:36`, no reference for the other two.

## Subsequences[edit | edit source]

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

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

**3.15 Definition**

means `s is non bounded_above` (`SEQ_2:def 1`). 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 , the second one maps extended real sequences to extended reals, thereby allowing . 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 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` () in combination with `RINFSUP2:28/29`.

## Some Special Sequences[edit | edit source]

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

**3.21 Definition**

The sum for can be expressed via `Sum(a, p, q)` (`SERIES_1:def 6`) if 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, 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 because they are `ManySortedSet of NAT` and `0 in NAT`. Inconvenient summands, like in the series of , 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[edit | edit source]

**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 is given by `SERIES_1:24` or `COMSEQ_3:64` for being real or complex respectively. No reference for .

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

**3.30 Definition**

is defined in `NEWTON:def 2`. is `number_e` (`POWER:def 4`), is `exp_R` (`SIN_COS:def 22`). 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[edit | edit source]

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

**3.38 Definition** No reference.

**3.39 Theorem** No reference.

**3.40 Examples** No reference.

## Summation By Parts[edit | edit source]

**3.41 Theorem** No reference.

**3.42 Theorem** No reference.

**3.43 Theorem** is `LEIBNIZ1:8`.

**3.44 Theorem** No reference.

## Absolute Convergence[edit | edit source]

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

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

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

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

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

**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**

, , and 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`, is `E --> c` (`FUNCOP_1:def 2`), with clusters in `VALUED_0`. 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[edit | edit source]

**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 (`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 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. is continuous by `NFCONT_1:17` (pointwise) and `NFCONT_1:28` (domain).

**4.12 Remark** Nothing to formalize.

## Continuity and Compactness[edit | edit source]

**4.13 Definition**

For real functions given by `RFUNCT_1:72`, for complex functions given by `SEQ_2:def 5`. For functions into 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**

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

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

**4.25 Definition**

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: having a discontinuity of the *first kind* at means `not f is_convergent_in x & f is_left_convergent_in x & f is_right_convergent_in x`; having a discontinuity of the *second kind* at means `not f is_left_convergent_in x or not f is_right_convergent_in x`.

**4.27 Examples**

(a) 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) 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) 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[edit | edit source]

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

**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`. , and are given by `LIMFUNC1:82/91`, `LIMFUNC1:87/96` and `LIMFUNC1:88/97` respectively.

## Exercises[edit | edit source]

1. No reference.

2. No reference, including no counterexample for the backwards direction. #TODO Show that .

3. 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, 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. 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 .

15. `open` is defined in `T_0TOPSP:def 2`. No reference for exercise.

16. is `[\x/]` (`INT_1:def 6`), is `frac x` (`INT_1:def 8`). No reference for exercise.

17. No reference.

18. No reference.

19. No reference.

20. 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[edit | edit source]

**5.1 Definition**

Mizar does not introduce differentiation via 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 .)

is differentiable at means `f is_differentiable_in x` (`FDIFF_1:def 4`), is `diff(f,x)` (`FDIFF_1:def 5`). is differentiable on means `f is_differentiable_on E` (`FDIFF_1:def 6`), 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**

for constant is `FDIFF_1:11/22`, see also `POLYDIFF:11`.

is `FDIFF_1:17`, see also `POLYDIFF:12`, and more general 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 has been explicitly excluded, no reference for that.

## Mean Value Theorems[edit | edit source]

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

**5.12 Theorem** No reference. #TODO implies the existence of an such that .

**Corollary** No reference.

## L'Hospital's Rule[edit | edit source]

**5.13 Theorem** in `L_HOSPIT`, especially `L_HOSPIT:10`.

## Derivatives of Higher Order[edit | edit source]

**5.14 Definition**

is `diff(f,E).n` (`TAYLOR_1:def 5`, see also `TAYLOR_1:def 6`), where is the domain on which is defined.

## Taylor's Theorem[edit | edit source]

**5.15 Theorem**

Set and , then is `Partial_Sums(Taylor(f,E,c,d)).(n-'1)` (see `SERIES_1:def 1` and `TAYLOR_1:def 7`), where is the domain on which is defined. The theorem is `TAYLOR_1:27` with instead of .

## Differentiation of vector-valued Functions[edit | edit source]

**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 and are given by `CFDIFF_1:23/28`, `CFDIFF_1:26/31` respectively. No reference for .

**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`.

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`.

is given by `NDIFF_3:14/17`. No reference for inner product.

**5.17 Examples** No reference. is defined in `SIN_COS:def 14`, is given by `SIN_COS:25`.

**5.18 Examples** No reference.

**5.19 Theorem** No reference.

## Exercises[edit | edit source]

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 implies .

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

**6.1 Definition**

A partition is described by a `Division` (`INTEGRA1:def 2`), leaving out and changing to . The intervals can be accessed via `divset(P,i)` (`INTEGRA1:def 4`), therefore is given by `vol divset(P,i)` (`INTEGRA1:def 5`).

is `upper_sum(f,P)` (`INTEGRA1:def 8`), is `lower_sum(f,P)` (`INTEGRA1:def 9`).

is `upper_integral(f)` (`INTEGRA1:def 14`), is `lower_integral(f)` (`INTEGRA1:def 15`).

being `integrable` is in `INTEGRA1:def 16` (see also `INTEGRA5:def 1`), 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 is bounded and integrable and is continuous, then is integrable.

## Properties of the Integral[edit | edit source]

**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 with .

(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**

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

**6.20 Theorem**

`INTEGRA6:28/29`, but no reference for the continuity of if 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[edit | edit source]

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

**6.26 Definition**

More generally, being a `parametrized-curve` is defined in `TOPALG_6:def 4`, no reference for closed curves there. For simple closed curves in 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 -curves using another approach.

No reference for or *rectifiable*.

**6.27 Theorem** No reference.

## Exercises[edit | edit source]

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

**7.1 Definition**

Let denote . being pointwise convergent is described by `F is_point_conv_on E` (`SEQFUNC:20`, see also `SEQFUNC:def 10`). Then 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[edit | edit source]

**7.7 Definition**

being uniformly convergent on 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[edit | edit source]

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

**7.16 Theorem** is `INTEGRA7:31` or `MESFUN10:21`.

**Corollary** No reference.

## Uniform Convergence and Differentiation[edit | edit source]

**7.17 Theorem** No reference. #TODO show that

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

## Equicontinuous Families of Functions[edit | edit source]

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

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

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

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

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. 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`).

is given by `POWER:def 3` or `TAYLOR_1:14/15`, is given by `TAYLOR_1:12/13` or `MOEBIUS3:16`. 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`. is given by `FDIFF_6:1`. No reference for being lower than any positive power of .

## The Trigonometric Functions[edit | edit source]

and are defined in `SIN_COS3:def 2` and `SIN_COS3:def 1` respectively. is given by `SIN_COS3:36` (or more general by `SIN_COS3:19`). is given by `SIN_COS:27`. No reference for derivates in complex case, but in real case given by `SIN_COS:63/64`. in Mizar is defined as the unique such that (`SIN_COS:def 28`). is given by `SIN_COS:76/77`, that 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[edit | edit source]

**8.8 Theorem** is `POLYNOM5:74`.

## Fourier Series[edit | edit source]

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

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

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

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

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

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

**9.24 Theorem** No reference.

**9.25 Theorem** No reference.

## The Implicit Function Theorem[edit | edit source]

**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