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

Limits of Functions

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

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

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

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

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

Remark No reference.

Continuous Functions

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

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

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

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

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

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

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

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

4.12 Remark Nothing to formalize.

Continuity and Compactness

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

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

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

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

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

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

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

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

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

Continuity and Connectedness

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

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

4.24 Example No reference.

Discontinuities

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

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

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

Monotonic Functions

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

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

Corollary No reference.

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

4.31 Remark No reference.

Infinite Limits and Limits at Infinity

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

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

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

Exercises

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