# Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Sequences and Series of Functions

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

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

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

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

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

**Corollary** No reference.

## Uniform Convergence and Differentiation edit

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

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

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

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.