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

Finite, Countable, And Uncountable Sets

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 $f$ is defined by FUNCT_1:def 1. $f(x)$ 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 $f$ 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
$f(E)$ is f.:E (RELAT_1:def 13, FUNCT_1:def 6), the remark is RELAT_1:113. $f(A)\subset B$ is encoded in RELSET_1. Onto is onto (FUNCT_2:def 3).
$f^{-1}(E)$ is f"E (RELAT_1:def 14, FUNCT_1:def 7). $f^{-1}(y)$ 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 $A$ and $B$ 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
$J_{n}$ is Seg n (FINSEQ_1:def 1), $J$ is NATPLUS (NAT_LAT:def 6), although it should be mentioned that in Mizar NAT (ORDINAL1:def 11, synonym introduced in NUMBERS) being $J\cup \{0\}$ 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 $X$ is finite by FINSEQ_1:56. If $X$ 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 $X$ 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 $X$ (but not necessarily a certain range), a ManySortedSet of X is a total X-defined Function (PBOOLE). Then a sequence in Mizar (starting with $0$ instead of $1$) is a ManySortedSet of NAT. If it is a sequence of elements of some $A$, 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 $E$ of subsets of $\Omega$ 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. $E_{1}\cup E_{2}$ is E1 \/ E2 (XBOOLE_0:def 3). The intersection of $E$ is meet E (SETFAM_1:def 1). $E_{1}\cap E_{2}$ is E1 /\ E2 (XBOOLE_0:def 4). $A$ and $B$ 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

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, $R^{k}$ as a metric space is Euclid n (EUCLID:def 7), $R^{1}$ is also RealSpace (METRIC_1:def 13).
Subsets of $Y$ 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
$(a,b)$ is ].a,b.[ (XXREAL_1:def 4), $[a,b]$ is [.a,b.] (XXREAL_1:def 1), $[a,b)$ is [.a,b.[ (XXREAL_1:def 2), $(a,b]$ is ].a,b.] (XXREAL_1:def 3).
A $k$-cell is cell(a,b) (CHAIN_1:def 6).
The open/closed ball with center $x$ and radius $r$ 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) "$p$ is a limit point of $E$" 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 $E$, the derivative of $E$, is Der E (TOPGEN_1:def 3), which gives a second characterization via TOPGEN_1:17.
(c) Just like that, "$p$ is a isolated point of $E$" 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 $E$ 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) ${\overline {E}}$ 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

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 $T_{2}$ 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 $R^{k}$, accumulation point variant.

2.42 Theorem No reference. #TODO Find the Weierstrass theorem for $R^{k}$, accumulation point variant.

2.43 Theorem No reference. #TODO Find that nonempty perfect subsets of $R^{k}$ are uncountable.

Corollary No reference, although $R$ 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

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

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 $E'$ there. If the topological space is $T_{1}$, $E'$ is closed (clustered in TOPGEN_1), $E''\subset E'$ (TOPGEN_1:32) and ${\overline {E'}}=E'$ (TOPGEN_1:33). No reference for $E'={\overline {E}}'$ or example of $E'\neq E''$.
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, $E^{\circ }$ is Int E (TOPS_1:def 1), see above.
9(a) $E^{\circ }$ 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 $A\cup B$ 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 $R^{k}$ 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.