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

## Finite, Countable, And Uncountable Sets edit

As mentioned before, the Book does not properly introduce relations. In Mizar, a function is a special kind of `Relation` (see `RELAT_1:def 1`), so many facts that seem obvious about functions hold more generally for relations, and are therefore in `RELAT_1` instead of `FUNCT_1`.

**2.1 Definition**

A `Function` is defined by `FUNCT_1:def 1`. is `f.x` (`FUNCT_1:def 2`). A `Function of A,B` is defined in `FUNCT_2`, it main properties are encoded by `FUNCT_2:def 1`, `RELAT_1:def 18` and `RELAT_1:def 19`. The domain/range of `dom f`/`rng f` is initially defined in `XTUPLE_0:def 12/13` and renamed in `RELAT_1`. `rng f` gets a helpful redefinition in `FUNCT_1:def 3`.

**2.2 Definition**

is `f.:E` (`RELAT_1:def 13`, `FUNCT_1:def 6`), the remark is `RELAT_1:113`. is encoded in `RELSET_1`. Onto is `onto` (`FUNCT_2:def 3`).

is `f"E` (`RELAT_1:def 14`, `FUNCT_1:def 7`). is `f"{y}` or `Coim(f,y)` (`RELAT_1:def 17`). There is no reference for the first definition in the Book of "one-to-one", but the second one is `FUNCT_1:def 4`.

**2.3 Definition**

The one-to-one correspondence of and is expressed by `A,B are_equipotent` (`WELLORD2`), that this is equivalent to their cardinality is `CARD_1:5`. Reflexivity and symmetry are encoded in `WELLORD2:def 4`, transitivity is `WELLORD2:15`. On the other hand, reflexivity, symmetry and transitivity of the cardinality are built in by the `=` predicate.

The properties of a `Relation` to be `reflexive`, `symmetric` and `transitive` are given by `RELAT_2:def 9`, `RELAT_2:def 11` and `RELAT_2:def 16` respectively. `Equivalence_Relation` is defined in `EQREL_1`. In Mizar, a `Relation` is a proper set and since a reflexive relation contains a copy of itself, the one-to-one correspondence of sets cannot be expressed in a `Relation` in Mizar since there is no set of sets.

**2.4 Definition**

is `Seg n` (`FINSEQ_1:def 1`), is `NATPLUS` (`NAT_LAT:def 6`), although it should be mentioned that in Mizar `NAT` (`ORDINAL1:def 11`, synonym introduced in `NUMBERS`) being is more commonly used. Nonnegative integers are usually used with `let n be Nat`, positive integers with `let n be non zero Nat` (`ORDINAL1:def 14`) instead of `let n be Element of NATPLUS`. Consequently, countability is defined with `NAT`.

(a) The definition is equivalent to the one in Mizar (`FINSET_1:def 1`). If `X is finite`, then is finite by `FINSEQ_1:56`. If is finite, then `card X = card Seg n = n` by (`FINSEQ_1:57`), then `card X is finite` (`natural -> finite` clustered in `CARD_1`) and hence `X is finite` (because for infinite `card X -> infinite` is clustered in `CARD_1`).

(b) is given as antonym of `finite` in `FINSET_1`.

(c) is `denumerable` (`CARD_3:def 15`).

(d) is given as antonym of `countable` in `CARD_3`.

(e) is `countable` (`CARD_3:def 14`).

**2.5 Example** is clustered in `GAUSSINT`.

**2.6 Remark** No reference. #TODO Find reference for `X is infinite iff ex Y being proper Subset of X st X,Y are_equipotent`

**2.7 Definition**

A function with a certain domain (but not necessarily a certain range), a `ManySortedSet of X` is a `total X-defined Function` (`PBOOLE`). Then a sequence in Mizar (starting with instead of ) is a `ManySortedSet of NAT`. If it is a sequence of elements of some , then it can also be described as a `sequence of A` (`NAT_1`).

The remark following afterwards is partly encoded in `DICKSON:3`, but there is no reference.

**2.8 Theorem** No reference. #TODO Find `let X be denumerable set; cluster infinite -> denumerable for Subset of X`

**2.9 Definition**

An indexed set family is a `ManySortedSet`, as described above. If just a set of subsets of is given, that would be a `Subset-Family` (`SETFAM_1`). Since any object is a set in Mizar, the functor `union E` (`TARSKI:def 4`) works without that notion. is `E1 \/ E2` (`XBOOLE_0:def 3`). The intersection of is `meet E` (`SETFAM_1:def 1`). is `E1 /\ E2` (`XBOOLE_0:def 4`). and intersect is `A meets B` (as antonym of the next predicate in `XBOOLE_0`), else `A misses B` (`XBOOLE_0:def 7`).

**2.10 Example**

(a) No reference.

(b) No reference.

**2.11 Remarks**

(8) is wired in the definitions `XBOOLE_0:def 3/4`.

(9) is `XBOOLE_1:4` and `XBOOLE_1:16`.

(10) is `XBOOLE_1:23` (and the other one is `XBOOLE_1:24`).

(11) is `XBOOLE_1:7`.

(12) is `XBOOLE_1:17`.

(13) is built in with the correct requirements.

(14) is `XBOOLE_1:12` and `XBOOLE_1:28`.

**2.12 Theorem** No reference. #TODO Find that union of set family is denumerable if each set in it is at most countable and at least one is denumerable

**Corollary** is `CARD_4:12`.

**2.13 Theorem** is `CARD_4:10`.

**Corollary** is `TOPGEN_3:17`.

**2.14 Theorem**`TOPGEN_3:29` in combination with `CARD_2:def 3` and `CARD_1:50` shows that the cardinality of the 0-1-sequences is the same as the cardinality of `REAL`. `TOPGEN_3:30` shows that that the reals are not denumerable.

## Metric Spaces edit

**2.15 Definition** is `MetrSpace` (`METRIC_1`), defined through `METRIC_1:def 6-9` (which refer to `METRIC_1:def 2-5` respectively).

**2.16 Examples**

As noted before, as a metric space is `Euclid n` (`EUCLID:def 7`), is also RealSpace (`METRIC_1:def 13`).

Subsets of as metrics spaces is done by `SubSpace of Y` (`TOPMETR:def 1`) and `TOPMETR:def 2`.

#TODO Reference the last two examples.

**2.17 Definition**

is `].a,b.[` (`XXREAL_1:def 4`), is `[.a,b.]` (`XXREAL_1:def 1`), is `[.a,b.[` (`XXREAL_1:def 2`), is `].a,b.]` (`XXREAL_1:def 3`).

A -cell is `cell(a,b)` (`CHAIN_1:def 6`).

The open/closed ball with center and radius is given by `Ball(x,r)`/`cl_Ball(x,r)` (`METRIC_1:def 14/15` for metric spaces and `TOPREAL9:def 1/2` for `TOP-REAL k`).

Convex sets are defined by `CONVEX1:def 2` (usable for `TOP-REAL k`, but not for `Euclid k`). The open/closed balls are clustered as convex in `TOPREAL9`. No reference for convexity of cells. #TODO Find it.

**2.18 Definition**

(a) is `Ball(p,r)` (`METRIC_1:def 14`)

(b) No reference.

(c) No reference.

(d) No reference.

(e) No reference.

(f) No reference.

(g) No reference.

(h) No reference.

(i) is `TBSP_1:def 7` or `METRIC_6:def 3`.

(j) No reference.

**2.18 Definition (for topological spaces and TOP-REAL k)**

The basics of topological spaces are in

`PRE_TOPC`.

(a) is

`Ball(p,r)`(

`TOPREAL9:def 1`)

(b) " is a limit point of " is basically

`p is_an_accumulation_point_of E`(

`TOPGEN_1:def 2`), this is shown with

`TOPS_1:12`. The set of all limit points of , the derivative of , is

`Der E`(

`TOPGEN_1:def 3`), which gives a second characterization via

`TOPGEN_1:17`.

(c) Just like that, " is a isolated point of " is

`p is_isolated_in E`(

`TOPGEN_1:def 4`).

(d) is

`TOPGEN_4:3`. A set is defined to be

`closed`in

`PRE_TOPC:def 3`.

(e) is

`TOPS_1:22`. The interior of is

`Int E`(

`TOPS_1:def 1`).

(f) is

`TOPS_1:23`. A set is defined to be

`open`in

`PRE_TOPC:def 2`.

(g) is

`SUBSET_1:def 4`, see also

`XBOOLE_0:def 5`.

(h) is

`TOPGEN_1:def 10`in combination with

`TOPGEN_1:def 7`. See also

`TOPS_1:5`and

`TOPGEN_1:28`. (i) No reference.

(j) given by

`TOPS_1:def 3`and

`TOPGEN_1:29`.

**2.19 Theorem** No reference.

**2.19 Theorem (for topological spaces and TOP-REAL n)** the balls of

`TOP-REAL k`are clustered open in

`TOPREAL9`.

**2.20 Theorem** No reference.

**2.20 Theorem (for topological spaces and TOP-REAL n)** No reference.

**Corrolary** No reference.

**Corrolary (for topological spaces and TOP-REAL n)** No reference.

**2.21 Examples** No reference. (Detailed list omitted here.)

**2.22 Theorem** is `SETFAM_1:33` or `TOPS_2:6`. Counterpart is `SETFAM_1:34` or `TOPS_2:7`.

**2.23 Theorem** No reference.

**2.23 Theorem (for topological spaces)** is `TOPS_1:4`.

**Corrolary** No reference.

**Corrolary (for topological spaces)** is `TOPS_1:3`.

**2.24 Theorem**

(a) No reference.

(b) No reference.

(c) No reference.

(d) No reference.

**2.24 Theorem (for topological spaces)**

(a) is `TOPS_2:19`.

(b) is `TOPS_2:22`.

(c) is `TOPS_2:20`.

(d) is `TOPS_2:21`.

**2.25 Examples** No reference.

**2.26 Definition** No reference.

**2.26 Definition (for topological spaces)** is `Cl E` (`PRE_TOPC:def 7`), the definition is `TOPGEN_1:29 `.

**2.27 Theorem**

(a) No reference.

(b) No reference.

(c) No reference.

**2.27 Theorem (for topological spaces)**

(a) is clustered in `TOPS_1`.

(b) is `PRE_TOPC:22`.

(c) is `TOPS_1:5`.

**2.28 Theorem** No reference.

**2.29 Remark** No reference.

**2.30 Theorem** given by `PRE_TOPC:def 4`.

## Compact Sets edit

**2.31 Definition** is `SETFAM_1:def 11`.

**2.32 Definition** No direct reference. `compact` is defined in `TOPMETR:def 5` via the topological definition. See also `TOPMETR:16`.

**2.32 Definition (for topological spaces)** is `COMPTS_1:def 1`. That finite sets are compact is clustered in `YELLOW13`.

**2.33 Theorem** No reference.

**2.33 Theorem (for topological spaces)** is `COMPTS_1:3`.

**2.35 Theorem** No reference.

**2.35 Theorem (for topological spaces)** is `COMPTS_1:7`.

**2.35 Theorem** No reference.

**2.35 Theorem (for topological spaces)** is `COMPTS_1:8`.

**Corollary** No reference.

**Corollary (for topological spaces)** No reference.

**2.36 Theorem** No reference.

**2.36 Theorem (for topological spaces)** is `COMPTS_1:4` with `FINSET_1:def 3`.

**Corollary** No reference.

**Corollary (for topological spaces)** No reference.

**2.37 Theorem** No reference.

**2.38 Theorem** is `COUSIN:35`.

**2.39 Theorem** No reference. #TODO Find that meet of nested cells is non empty.

**2.40 Theorem** No reference. #TODO Find that cells are compact.

**2.41 Theorem** No reference. #TODO Find the Heine-Borel theorem for , accumulation point variant.

**2.42 Theorem** No reference. #TODO Find the Weierstrass theorem for , accumulation point variant.

**2.43 Theorem** No reference. #TODO Find that nonempty perfect subsets of are uncountable.

**Corollary** No reference, although being uncountable was discussed in commentary to Theorem 2.14. #TODO Real intervals are uncountable.

**2.44 The Cantor set** see `CANTOR_1`. It seems the definition of `the_Cantor_set` (`CANTOR_1:def 5`) isn't designed to be a subset of the reals.

## Connected Sets edit

**2.45 Definition** No reference.

**2.45 Definition (for topological spaces)** is `CONNSP_1:def 1` and `CONNSP_1:def 3`.

**2.46 Remark** is `CONNSP_1:1`. An example quite similar to the one given in the Book is given by `BORSUK_4:17`.

**2.47 Theorem**

First two clusterings. `pathwise_connected -> connected` in `BORSUK_2`, `interval -> pathwise_connected` in `TOPALG_2`. Now an `interval` has the described properties (`XXREAL_2:80`) and the given properties describe an `interval` (`XXREAL_2:84`). Note difference between `XXREAL_2:def 12` and `TOPALG_2:def 3`.

## Exercises edit

1. is `XBOOLE_1:2`.

2. Algebraic numbers are given through `ALGNUM_1:def 2` and `ALGNUM_1:def 4`. #TODO Find that the set of algebraic numbers is countable.

3. Existence of `liouville` (`LIOUVIL1:def 5`) numbers is clustered in `LIOUVIL1`. `transcendental` is introduced as antonym in `ALGNUM_1`, and liouville numbers are clustered as transcendential in `LIOUVIL2`.

4. No reference. #TODO Find that irrational numbers have cardinality of continuum.

5. No reference.

6. No reference for metric spaces, since no reference for there. If the topological space is , is closed (clustered in `TOPGEN_1`), (`TOPGEN_1:32`) and (`TOPGEN_1:33`). No reference for or example of .

7. No reference for metric spaces. For topological spaces, no reference for finite version (except `PRE_TOPC:20`), infinite version is `TDLAT_2:15`.

8. No reference.
9. No refence for metric spaces. For topological spaces, is `Int E` (`TOPS_1:def 1`), see above.

9(a) open is clustered in `TOPS_1`.

9(b) is `TOPS_1:23`.

9(c) is `TOPS_1:24`.

9(d) is `TOPS_1:def 1`.

9(e) is `supercondensed` (`ISOMICHI:def 1`).

9(f) is `subcondensed` (`ISOMICHI:def 2`).

10. is `METRIC_1:def 10/11`. No reference for open/closed/compact sets.

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 for metric spaces. For topological spaces:

19(a) is `CONNSP_1:2`.

19(b) if is the whole space, `CONNSP_1:3`.

19(c) No reference.

19(d) No reference.

20. No reference.

21(a) No reference.

21(b) No reference.

21(c) No reference.

21(d) No reference.

22. No reference for metric spaces. `separable` is defined by `TOPGEN_1:def 12` and `TOPGEN_1:def 13`. Separability of is given by a series of clusters. `TOP-REAL k` is clustered `second-countable` (`WAYBEL23:def 6`) in `MFOLD_0`. `second-countable -> Lindelof` (`METRIZTS:def 2`) in `METRIZTS`. `Lindelof -> separable` in `METRIZTS` if the topological space is metrizable. No reference for `TOP-SPACE k` being `metrizable` (`PCOMPS_1:def 8`).

23. No reference for metric spaces. `Basis` of a topological space is defined in `CANTOR_1`. No reference for the statement. #TODO Find that every separable metric space has countable base.

24. No reference.

25. No reference.

26. No reference.

27. No reference for metric spaces. Condensation points of topological spaces are defined in `TOPGEN_4:def 9`. The set of condensation points is defined in `TOPGEN_4:def 10`. No reference for statement.

28. No reference.

29. No reference.

30. No reference.