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

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

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

## Discontinuities

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

## Exercises

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