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

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

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

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

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

**Corollary** No reference.

## Uniform Convergence and DifferentiationEdit

**7.17 Theorem** No reference. #TODO show that

**7.18 Theorem** No reference. #TODO existence of continuous nowhere differentiable function

## Equicontinuous Families of FunctionsEdit

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

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

## ExercisesEdit

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.