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

From Wikibooks, open books for an open world
Jump to navigation Jump to search

Limits of Functions[edit]

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.

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]

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]

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]

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.


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]

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]

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.


1. No reference.
2. No reference, inclusing 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.