Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/The Real and Complex Number Systems

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.