Topology Rosetta Stone - Mizar

• Definition. A Topology on a set \(X\) is a family of subsets \(\mathcal{T}\) such that

  1. \(X\in\mathcal{T}\) and \(\emptyset\in\mathcal{T}\)
  2. for any family of subsets of \(\mathcal{T}\), their union is also in \(\mathcal{T}\)
  3. intersections of finitely man elements of \(\mathcal{T}\) are also in \(\mathcal{T}\)

  Together, \(X\) and a particular topology form a Topological Space

  • The idiomatic Mizar formalization begins with defining the data as TopStruct and the axioms as an attribute TopSpace-like, then bundle them together as a TopSpace.
  • Remember, for 1-sorted objects X, we write [#] X for the underlying set, and we write {} X for the empty subset of the underlying set.
  • We don't actually need to specify \(\emptyset\in\mathcal{T}\) as this can be proven (PRE_TOPC:1).
• Definition. Given a topological space \((X, \mathcal{T})\) we say a subset \(U\subset X\) is Open if it is a member of the topology \(U\in\mathcal{T}\) (PRE_TOPC:def 2)
• Example: the discrete topology (TDLAT_3:def 1) is just the powerset, and the ant-discrete topology (TDLAT_3:def 2) is just \(\{X,\emptyset\}\)
• Example: Finite-complement topology doesn't seem to be formalized in Mizar
• Definition. Let \(\mathcal{T}_{1}\) and \(\mathcal{T}_{2}\) be topologies on the same set \(X\). Then we say \(\mathcal{T}_{1}\) is Finer than \(\mathcal{T}_{2}\) if \(\mathcal{T}_{1}\subset\mathcal{T}_{2}\) (SETFAM_1:def 2) and we say \(\mathcal{T}_{2}\) is Coarser than \(\mathcal{T}_{1}\) (SETFAM_1:def 3).

• Implicit Definition. Let \(X\) be a non-empty set and \(A\) be a family of subsets of \(X\). We call the Union Closure of \(A\) to be a subset family of \(X\) denoted \(\operatorname{UniCl}(A)\) such that \(x\in\operatorname{UniCl}(A)\) iff there exists a family \(Y\) of subsets of \(X\) such that \(Y\subset A\) and \(x\in \bigcup Y\) (CANTOR_1:def 1).
• Implicit Definition. Let \(X\) be a non-empty set and \(A\) a family of subsets of \(X\). We call the Finite-intersection closure of \(A\) to be a subset family of \(X\) denoted \(\operatorname{FinMeetCl}(A)\) such that \(x\in\operatorname{FinMeetCl}(A)\) iff there is a family \(Y\) of subsets of \(X\) such that \(Y\subset A\) and \(Y\) is finite and \(x\in\bigcap Y\) (CANTOR_1:def 3).

• Definition. Let \(X\) be a set. A Basis for some topology on \(X\) is a family \(\mathcal{B}\) of subsets of \(X\) such that

  1. for each \(x\in X\) there exists a \(B\in\mathcal{B}\) such that \(x\in B\)
  2. for each \(x\in X\) and \(B_{1},B_{2}\in\mathcal{B}\) such that \(x\in B_{1}\cap B_{2}\), there exists a \(B_{3}\in\mathcal{B}\) such that \(x\in B_{3}\) and \(B_{3}\subset B_{1}\cap B_{2}\).

  Then the Topology Generated by \(\mathcal{B}\) is defined as the family \(\mathcal{T}\) of subsets of \(X\) such that for each \(U\subset X\) we have \(U\in\mathcal{T}\) iff for each \(x\in X\) such that \(x\in U\) there exists a basis element \(B\in\mathcal{B}\) such that \(x\in B\subset U\).

  • Mizar defines the basis for a topological space in CANTOR_1 as a family of open sets (which makes it a subset of the topology) such that the topology is a subset of its union closure (CANTOR_1:def 2) which is a fancy way to say its union closure is the topology.
• Lemma 13.1. Let \(X\) be a set, \(\mathcal{B}\) a basis for a topology \(\mathcal{T}\) on \(X\). Then \(\mathcal{T}\) is the collection of all possible unions of elements of \(\mathcal{B}\) (i.e., \(\mathcal{T}\) is the union closure of \(\mathcal{B}\)). (This can be taken as the defining property of the basis, CANTOR_1:def 2)
• Lemma 13.2. Let \((X,\mathcal{T})\) be a topological space, let \(\mathcal{C}\) be a collection of subsets of \(X\). If for each \(x\in X\) and for each \(U\in\mathcal{T}\) such that \(x\in U\) there exists a \(C\in\mathcal{C}\) such that \(x\in U\subset C\), then \(\mathcal{C}\) is a basis for \((X, \mathcal{T})\). Missing from Mizar
• Lemma 13.3. Let \(\mathcal{T}_{1}\), \(\mathcal{T}_{2}\) be topologies on \(X\) with bases \(\mathcal{B}_{1}\), \(\mathcal{B}_{2}\) respectively. Then \(\mathcal{T}_{2}\) is finer than \(\mathcal{T}_{1}\) if and only if for each \(x\in X\) and \(B_{1}\in\mathcal{B}_{1}\) there exists a \(B_{2}\in\mathcal{B}_{2}\) such that \(x\in B_{2}\) and \(B_{2}\subset B_{1}\). Missing from Mizar
• Definition. The Standard Topology on \(\mathbb{R}\) is the topology generated by the basis \(\mathcal{B}=\{(a,b)\mid a,b\in\mathbb{R}\}\) given by all open intervals of \(\mathbb{R}\).
  • Mizar defines the real numbers equipped with the standard topology as the topological space R^1 (TOPMETR:def 6).
• Neither the lower-limit topology (generated by all intervals \([a,b)\)) nor the K-topology appear to be defined in Mizar. Missing from Mizar
• Lemma 13.4. \(\mathbb{R}_{\ell}\) and \(\mathbb{R}_{K}\) are finer than \(\mathbb{R}\), but incomparable to each other.

• Definition. A Subbasis (or Prebasis) \(\mathcal{S}\) for a topology on \(X\) is a collection of subsets of \(X\) such that \(\bigcup\mathcal{S}=X\) (CANTOR_1 and CANTOR_1:def 4).

  The Topology Generated by a Prebasis is the collection \(\mathcal{T}\) of arbitrary unions of finite intersections of subbasis elements. (CANTOR_1:18)

• Definition. Let \((X,\mathcal{T}_{X})\) and \((Y,\mathcal{T}_{Y})\) be topological spaces. The Product Topology on \(X\times Y\) is the topology having as its basis the collection \(\mathcal{B}\) of all sets of the form \(U\times V\) where \(U\in\mathcal{T}_{X}\) and \(V\in\mathcal{T}_{Y}\). We call \(X\times Y\) equipped with the product topology the Product Space.
  • The Cartesian product \(X\times Y\) of sets in Mizar is [:X,Y:]
  • The product space is defined in BORSUK_1:def 2
• Theorem 15.1. Let \(\mathcal{B}\) be a basis for \((X,\mathcal{T}_{X})\) and \(\mathcal{C}\) be a basis for \((Y,\mathcal{T}_{Y})\). Then the collection \(\mathcal{D}=\{B\times C\mid B\in\mathcal{B},C\in\mathcal{C}\}\) is a basis for the product topology on \(X\times Y\). Missing from Mizar
• Definition. The Projection Maps \(\pi_{1}\colon X\times Y\to X\) and \(\pi_{2}\colon X\times Y\to Y\) defined by \(\pi_{1}(x,y)=x\) and \(\pi_{2}(x,y)=y\) for \(x\in X\) and \(y\in Y\).
  • \(\pi_{1}\) is pr1 (X,Y) defined in FUNCT_3:def 4
  • \(\pi_{2}\) is pr2 (X,Y) in Mizar, defined in FUNCT_3:def 5
  • The induced projection mappings on the topologies are defined as Pr1(X,Y) and Pr2(X,Y) in BORSUK_1:def 4 and BORSUK_1:def 5 and its defining property may be found in Theorem BORSUK_1:24.
• Theorem 15.2. The collection \(\mathcal{S}=\{\pi_{1}^{-1}(U)\mid U\in\mathcal{T}_{X}\}\cup\{\pi_{2}^{-1}(V)\mid V\in\mathcal{T}_{Y}\}\) is a prebasis for the product topology on \(X\times Y\). Missing from Mizar

• Definition. Let \((X,\mathcal{T})\) be a topological space, let \(Y\subset X\). Then we define the Subspace Topology of \(Y\) consists of the collection \(\mathcal{T}_{Y}=\{Y\cap U\mid U\in\mathcal{T}\}\) and it forms a topology on \(Y\). We refer to the topological space \((Y,\mathcal{T}_{Y})\) as a Subspace of \(X\).
  • Mizar defines SubSpace of T in PRE_TOPC:def 4.
• Lemma 16.1. If \(\mathcal{B}\) is a basis for the topology of \(X\), then \(\mathcal{B}_{Y}=\{B\cap Y\mid B\in\mathcal{B}\}\) is a basis for the subspace topology of \(Y\). Missing from Mizar
• Lemma 16.2. Let \((Y,\mathcal{T}_{\text{sub}})\) be a subspace of \((X,\mathcal{T})\). If \(U\) is open in \(Y\) and \(Y\) is open in \(X\), then \(U\) is open in \(X\). (TSEP_1:18 proves more than this)
• Theorem 16.3. If \(A\) is a subspace of \(X\) and \(B\) is a subspace of \(Y\), then the product topology on \(A\times B\) is the same as the topology \(A\times B\) inherits as a subspace of \(X\times Y\). (BORSUK_3:22)

• Definition. Let \((X,\mathcal{T})\) be a topological space, let \(A\) be a subset of \(X\). We say \(A\) is Closed if its complement \(X\setminus A\) is open. (PRE_TOPC:def 3)
• Theorem 17.1. Let \((X,\mathcal{T})\) be a topological space. Then:
  1. \(\emptyset\) is closed (registered in PRE_TOPC)
  2. \(X\) is closed (registered in PRE_TOPC)
  3. Arbitrary intersections of sets are closed (PRE_TOPC:14 and TOPS_2:22)
  4. Finite unions of closed sets are closed (TOPS_2:21)
• Theorem 17.2. Let \((Y,\mathcal{T}_{\text{sub}})\) be a subspace of \((X,\mathcal{T})\). Then a set \(A\) is closed in \(Y\) iff there is a closed subset \(B\subset X\) such that \(A=B\cap Y\). Missing from Mizar
• Theorem 17.3. Let \((Y,\mathcal{T}_{\text{sub}})\) be a subspace of \((X,\mathcal{T})\). If \(A\) is closed in \(Y\) and \(Y\) is closed in \(X\), then \(A\) is closed in \(X\).
  • TSEP_1:8 proves something more: let \(X_{0}\) is a subspace of \(X\), let \(A\subset X\), \(C\subset X\), and \(B\subset X_{0}\) be \(B=A\) considered as a subset of \(X_{0}\). If \(C\subset X_{0}\) and \(C\) is closed in \(X\), then \(A\) is closed in \(X\) iff \(B\) is closed in \(X_{0}\).
• Definition. Let \((X,\mathcal{T})\) be a topological space, let \(A\) be a subset of \(X\).
  1. The Closure of \(A\) is the subset \(\operatorname{Cl}(A)\) of \(X\) equal to the intersection of all closed subsets of \(X\) containing \(A\) (PRE_TOPC:16 proves the logical equivalence; TOPS_1 registers it is a closed subset of \(X\).)
     • Cl A is defined in PRE_TOPC:def 7
  2. The Interior of \(A\) is the subset \(\operatorname{Int}(A)\) of \(X\) equal to the union of all open subsets of \(X\) contained in \(X\) (TEX_4:3 proves this logical equivalence)
     • Int A is defined as \(X\setminus\operatorname{Cl}(X\setminus A)\) in TOPS_1:def 1
• Theorem 17.4. Let \((Y,\mathcal{T}_{\text{sub}})\) be a subspace of \((X,\mathcal{T})\). Let \(A\) be a subset of \(Y\), \(B\) a subset of \(X\) such that \(A=B\). Then \(\operatorname{Cl}(A)=\operatorname{Cl}(B)\cap Y\). Missing from Mizar
• Theorem 17.5. Let \(A\) be a subset of \((X,\mathcal{T})\).
  1. Then \(x\in\operatorname{Cl}(A)\) iff every open subset \(U\) of \(X\) containing \(x\) intersects \(A\) (this is the definition found in PRE_TOPC:def 7)
  2. If \(\mathcal{B}\) is a basis generating \(\mathcal{T}\), then \(x\in\operatorname{Cl}(A)\) iff every basis element \(B\in\mathcal{B}\) containing \(x\in B\) intersects \(A\). Missing from Mizar
• Definition. If \(A\) is a subset of \((X,\mathcal{T})\) and if \(x\in X\), we say \(x\) is a Limit Point of \(A\) (or \(x\) is an Accumulation Point of \(A\)) if every neighborhood of \(x\) intersects \(A\) in some other point than \(x\) — i.e., if \(x\in\operatorname{Cl}(A\setminus\{x\})\). (TOPGEN_1:def 2)
• Implicit Definition. The Derivative of a set \(A\) is the set of limit points of \(A\) and denoted \(\operatorname{Der}(A)\). (TOPGEN_1:def 3)
• Theorem 17.6. Let \(A\) be a subset of a topological space \((X,\mathcal{T})\). Let \(A'\) be the set of limit points of \(A\). Then \(A\cup A'=\operatorname{Cl}(A)\). (TOPGEN_1:29)
• Corollary 17.7. A subset of a topological space is closed iff it contains all its limit points (TOPGEN_4:3)
• Definition. A topological space \((X,\mathcal{T})\) is called Hausdorff (or \(T_{2}\)) if for each distinct pair of points \(x_{1},x_{2}\in X\) there exists open sets \(U_{1}\in\mathcal{T}\) and \(U_{2}\in\mathcal{T}\) such that \(x_{1}\in U_{1}\) and \(x_{2}\in U_{2}\) and \(U_{1}\cap U_{2}=\emptyset\).
  • PRE_TOPC:def 10 defines T_2
  • COMPTS_1 introduces Hausdorff as a synonym for T_2
• Theorem 17.8. Every finite point set in a Hausdorff space \((X,\mathcal{T})\) is closed.
  • PCOMPS_1:7 proves singleton subsets are closed, then we can use previous results to establish the claim.
• Implicit Definition. The \(T_{1}\) property is defined and found in PRE_TOPC:def 9.
• Theorem 17.9. Let \((X,\mathcal{T})\) be a \(T_{1}\) space, let \(A\) be a subset of \(X\). Then a point \(x\) is a limit point of \(A\) iff every neighborhood of \(x\) contains infinitely many points of \(A\). Missing from Mizar
• Theorem 17.10. If \((X,\mathcal{T})\) is a Hausdorff space, then a sequence of points converges to at most one point of \(X\).
  • FRECHET_2:24 proves this
  • FRECHET2:def 2 defined convergent for a sequence of points
• Theorem 17.11.
  1. Every simply ordered set is a Hausdorff space in the order topology. Missing from Mizar
  2. The product of 2 Hausdorff spaces is a Hausdorff space (registered in BORSUK_2)
  3. A subspace of a Hausdorff space is Hausdorff (registered in JORDAN)
• Implicit Definition. Let \((X, \mathcal{T})\) be a topological space and \(A\subset X\) be a subset. We define the Boundary of \(A\) by the equation \(\partial A = \operatorname{Cl}(A)\cap\operatorname{Cl}(X\setminus A)\).
  • I think Bourbaki uses the symbol \(\operatorname{Fr}(A)\) instead of \(\partial A\), because the French word for "boundary" is frontière.
  • TOPS_1:def 2 uses the complement \(A^{\complement} = X\setminus A\) in its definition, but is otherwise what we have written down.
  • Many results concerning the boundary may be found in TOPS_1

• Definition. Let \((X,\mathcal{T}_{X})\) and \((Y,\mathcal{T}_{Y})\) be topological spaces, \(f\colon X\to Y\) be a function. We say \(f\) is Continuous if for each \(V\in\mathcal{T}_{Y}\), its preimage under \(f\) is open in \(X\), i.e., \(f^{-1}(V)\in\mathcal{T}_{X}\)
  • TOPS_2:43 proves this logical equivalence
• Theorem 18.1. Let \((X,\mathcal{T}_{X})\) and \((Y,\mathcal{T}_{Y})\) be topological space, let \(f\colon X\to Y\). Then the following are logically equivalence:
  1. \(f\) is continuous
  2. For every subset \(A\) of \(X\), we have \(f(\operatorname{Cl}(A))\subset\operatorname{Cl}(f(A))\) (TOPS_2:45)
  3. For every subset \(B\) of \(Y\), we have \(f^{-1}(Y)\) be closed in \(X\) (PRE_TOPC:def 6)
  4. For each \(x\in X\) and \(V\in\mathcal{T}_{Y}\) containing \(f(x)\in V\), there is a \(U\in\mathcal{T}_{X}\) such that \(f(U)\subset V\) (TMAP_1:43, TMAP_1:44)

• Definition. Let \(f\colon X\to Y\) be a map of topological spaces. We call \(f\) a Homeomorphism if \(f\) is a bijection and \(f\) is continuous and \(f^{-1}\) is continuous. (TOPS_2:def 5)

  In this case, we say \(X\) and \(Y\) are Homeomorphic. (T_0TOPSP:def 1)

  • BORSUK_3 establishes reflexivity, symmetry of are_homeomorphic
  • BORSUK_3:3 proves transitivity of are_homeomorphic, establishing it is an equivalence relation
• Definition. Let \((X,\mathcal{T}_{X})\) and \((Y,\mathcal{T}_{Y})\) be topological space, let \(f\colon X\to Y\) be a continuous function. We call \(f\) an Embedding if it is a homeomorphism onto its image \(f(X)\) considered as a subspace of \(Y\) equipped with the subspace topology. (COMPACT1:def 7)
• Theorem 18.2. Let \((X,\mathcal{T}_{X})\), \((Y,\mathcal{T}_{Y})\), \((Z,\mathcal{T}_{Z})\) be topological spaces.
  1. \(f\colon X\to Y\) mapping all of \(X\) to a single point is continuous (registered in PRE_TOPC)
  2. If \(A\) is a subspace of \(X\), then the inclusion mapping \(j\colon A\to X\) is continuous (TMAP_1:87)
  3. If \(f\colon X\to Y\) and \(g\colon Y\to Z\) are both continuous, then \(g\circ f\colon X\to Z\) is continuous (TOPS_2:46)
  4. If \(f\colon X\to Y\) is continuous and \(A\) is a subspace of \(X\), then \(f|_{A}\colon A\to Y\) defined by \(f|_{A}(a)=f(a)\) for \(a\in A\) is continuous (registered in TMAP_1)
  5. If \(f\colon X\to Y\) is continuous and \(Z\) is a subspace of \(Y\) containing \(f(X)\subset Z\), then \(g\colon X\to Z\) defined by \(f(x)=g(x)\) for all \(x\in X\) is continuous
  6. If \(f\colon X\to Y\) is continuous and \(Z\) is a space with \(Y\) as a subspace of \(Z\), then the function \(h\colon X\to Z\) defined by \(h(x)=f(x)\) for each \(x\in X\) is continuous (this is just \(h=j\circ f\) and follows from previous results, see TMAP_1:86)
  7. The map \(f\colon X\to Y\) is continuous if \(X\) can be written as the union of open sets \(U_{\alpha}\) such that \(f|_{U_{\alpha}}\) is continuous for each \(\alpha\) Missing from Mizar
• Theorem 18.3 (Pasting Lemma). Let \((X,\mathcal{T}_{X})\) and \((Y,\mathcal{T}_{Y})\) be topological spaces. Let \(X=A\cup B\) where \(A\) and \(B\) are closed in \((X,\mathcal{T})\). Let \(f\colon A\to Y\) and \(g\colon B\to Y\) be continuous functions. If \(f(x)=g(x)\) for every \(x\in A\cap B\), then \(f\) and \(g\) combine to give a continuous function \(h\colon X\to Y\) by setting \(h(x)=f(x)\) if \(x\in A\) and \(h(x)=g(x)\) if \(x\in B\). (TMAP_1:134)
• Theorem 18.4. Let \((A, \mathcal{T}_{A})\), \((X,\mathcal{T}_{X})\), and \((Y,\mathcal{T}_{Y})\) be topological spaces. Let \(f\colon A\to X\times Y\) be defined by \(f(a)=(f_{1}(a),f_{2}(a))\). Then \(f\) is continuous iff the functions \(f_{1}\colon A\to X\) and \(f_{2}\colon A\to Y\) are continuous. Missing from Mizar
  • In Mizar, f = <:f1,f2:> according to FUNCT_3:def 7.

• Definition. Let \(J\) be an indexing set. Given a set \(X\) we define a J-tuple of X to be a function \(\mathbf{x}\colon J\to X\). If \(\alpha\in J\), then we write \(x_{\alpha}\) instead of \(\mathbf{x}(\alpha)\) and this is called the α coordinate of x. The set of all \(J\) tuples of \(X\) is denoted \(X^{J}\).
  • This is just saying that \(\mathbf{x}\) is a function from \(J\) to \(X\), and it's the convention taken by Mizar.
• Definition. Let \(\{A_{\alpha}\}_{\alpha\in J}\) be an indexed family of sets. The Cartesian Product of this indexed family, denoted \(\prod_{\alpha\in J}A_{\alpha}\), is defined to be the set of all \(J\) tuples \((x_{\alpha})_{\alpha\in J}\) elements of \(X=\bigcup_{\alpha\in J}A_{\alpha}\) such that \(x_{\alpha}\in A_{\alpha}\) for each \(\alpha\in J\). (CARD_3:def 5)
• Definition. Let \(\{X_{\alpha}\}_{\alpha\in J}\) be an indexed family of topological spaces. Let us take as a basis for a topology on the product set \(\prod_{\alpha\in J}X_{\alpha}\) the collections of the form \(\prod_{\alpha\in J}U_{\alpha}\) where \(U_{\alpha}\subset X_{\alpha}\) is open for each \(\alpha\in J\). The topology generated by this is called the Box Topology. Missing from Mizar
• Definition. Let \(\{X_{\alpha}\}_{\alpha\in J}\) be an indexed family of topological spaces. Let \(\mathcal{S}_{\beta}\) denote the collection \(\mathcal{S}_{\beta}=\{\pi^{-1}_{\beta}(U_{\beta})\mid U_{\beta}\subset X_{\beta}~\mbox{open}\}\) and let \(\mathcal{S}=\bigcup_{\beta\in J}\mathcal{S}_{\beta}\). The topology generated by the prebasis \(\mathcal{S}\) is called the Product Topology and the resulting topological space \((\prod_{\alpha\in J}X_{\alpha},\mathcal{T}_{\text{prod}})\) is called the Product Space.
  • (WAYBEL18:def 2) defines the prebasis for the product topology
  • (WAYBEL18:def 3) defines the product space
• Theorem 19.1. (Comparison of box and product topologies…)
• Theorem 19.3. Let \(A_{\alpha}\) be subspaces of \(X_{\alpha}\) for each \(\alpha\in J\). Then \(\prod A_{\alpha}\) is a subspace of \(\prod X_{\alpha}\). (TOPS_5:82)
• Theorem 19.4. If each \(X_{\alpha}\) is a Hausdorff space, then \(\prod X_{\alpha}\) is a Hausdorff space in both the product and box topologies.
  • PRE_TOPC registers all Hausdorff spaces are \(T_{1}\) and YELLOW14:38 proves the product of \(X_{\alpha}\) all being \(T_{1}\) is a \(T_{1}\) space.
• Theorem 19.5. Let \(\{X_{\alpha}\}_{\alpha\in J}\) be a family of topological spaces, let \(A_{\alpha}\subset X_{\alpha}\) be a subset for each \(\alpha\in J\). If \(\prod X_{\alpha}\) is given either the box topology or product topology, then \(\prod\operatorname{Cl}(A_{\alpha}) = \operatorname{Cl}(\prod A_{\alpha})\). Missing from Mizar
• Theorem 19.6. Let \(f\colon A\to\prod X_{\alpha}\) be given by the equation \(f(a)=(f_{\alpha}(a))_{\alpha\in J}\) where \(f_{\alpha}\colon A\to X_{\alpha}\) for each \(\alpha\). Let \(\prod X_{\alpha}\) be given the product topology. Then the function \(f\) is continuous iff each \(f_{\alpha}\) is continuous. (WAYBEL18:6)
• Example 2: defines \(\mathbb{R}^{\omega}=\prod_{n\in\mathbb{N}}X_{n}\) where \(X_{n}=\mathbb{R}\).

• Definition. Let \(X\) be a set. A Metric on \(X\) is a function \(d\colon X\times X\to\mathbb{R}\) satisfying:
  1. \(d(x,x)\geq0\) for every \(x\in X\)
  2. \(d(x,y)=d(y,x)\) for every \(x,y\in X\)
  3. \(d(x,y)+d(y,z)\geq d(x,z)\) for every \(x,y,z\in X\)
• Given a metric \(d\) on a set \(X\), we call \((X,d)\) a Metric Space
  • As per idiomatic Mizar, METRIC_1 defines MetrStruct which is the pair (X,d) and bundles the appropriate attributes atop it to form MetrSpace in a separate definition.
• We call \(d(a,b)\) the distance between \(a\) and \(b\) (METRIC_1:def 1)
• Definition. Let \(d\) be a metric on \(X\), let \(\varepsilon\gt0\) be real, let \(x_{0}\in X\). We define the \(\varepsilon\) Ball centered at \(x_{0}\) to be the set \(B_{d}(x_{0},\varepsilon)=\{y\in X\mid d(x_{0},y)\lt\varepsilon\}\). (METRIC_1:def 14)
  • Tdisk is defined as the closed ball in TOP-REAL n
  • Tball is defined as the open ball in TOP-REAL n
• Definition. Let \((X,d)\) be a metric space. The collection \(\mathcal{B}=\{B_{d}(x,\varepsilon)\mid x_{0}\in X, \varepsilon\gt0\}\) forms the basis for the Metric Topology on \(X\) induced by \(d\).
  • PCOMPS_1:def 4 gives the definition Family_open_set for the basis
  • PCOMPS_1:def 5 gives us the topological space \((X,\mathcal{T}_{\text{met}})\) for the metric space \((X,d)\).
• Definition. Let \((X,\mathcal{T})\) be a topological space. We say \(X\) is Metrizable if there exists a metric \(d\) on \(X\) such that the metric topology induced by \(d\) is equal to the topology \(\mathcal{T}\). (PCOMPS_1:def 8)

• Definition. Let \((X,d)\) be a metric space. A subset \(A\subset X\) is called Bounded if there is some number \(M\gt0\) such that \(d(a_{1},a_{2})\leq M\) for every \(a_{1},a_{2}\in A\). (TBSP_1:def 6)

  If \(A\) is bounded and nonempty, the Diameter of \(A\) is defined to be \(\operatorname{diam}(A)=\sup\{d(a,b)\mid a,b\in A\}\). (TBSP_1:def 8)

• Theorem 20.1. Let \((X,d)\) be a metric space. Let \(\bar{d}\colon X\times X\to\mathbb{R}\) be defined by \(\bar{d}(x,y)=\min\{d(x,y),1\}\). Then \(\bar{d}\) is a metric on \(X\) which induces the same metric topology as \(d\). Missing from Mizar
  • We call \(\bar{d}\) the Standard Bounded Metric associated with \(d\). There is a more general notion formalized in Mizar: if \(r\gt0\) is some real number, \(\bar{d}_{r}(x,y)=\min\{d(x,y),r\}\) is shown to be a metric in NAGATA_1:31.

• Definition. Let \(\vec{x}=(x_{1},\dots,x_{n})\in\mathbb{R}^{n}\). We define the Norm of \(\vec{x}\) by \(\|\vec{x}\|=(x_{1}^{2}+\dots+x_{n}^{2})^{1/2}\). (EUCLID:def 5)

  We define the Euclidean Metric (or Pythagorean metric) on \(\mathbb{R}^{n}\) by \(d(x,y) = \|x-y\|\). (EUCLID:def 6 and EUCLID:21 proves it is a metric)

  We define the \(\ell_{\infty}\) metric (or Square Metric) by \(\rho(x,y)=\max\{|x_{1}-y_{1}|, \dots, |x_{n}-y_{n}|\}\). (SRINGS_5:def 20 and proves it is a metric on \(\mathbb{R}^{n}\) in SRINGS_5:95)

  • Note: \((\mathbb{R}^{n}, d)\) as a metric space is defined as Euclid n (EUCLID:def 7)
  • TOP-REAL n refers to \(\RR^{n}\) as a topological vector space whose underlying topological space coincides with that of the metric space topology induced by the Euclidean metric (EUCLID:def 8)
• Lemma 20.2. Let \(d_{1}\) and \(d_{2}\) be metrics on \(X\), let \(\mathcal{T}_{1}\) and \(\mathcal{T}_{2}\) be the associated metric topologies. Then \(\mathcal{T}_{1}\subset\mathcal{T}_{2}\) if and only if for each \(x\in X\) and \(\varepsilon\gt0\) there is a \(\delta\gt0\) such that \(B_{d_{1}}(x,\delta)\subset B_{d_{2}}(x,\varepsilon)\). Missing from Mizar
• Theorem 20.3. The topologies induced by the Euclidean and square metrics on \(\mathbb{R}^{n}\) are the same as the product topology on \(\mathbb{R}^{n}\).
  • EUCLID_9:28 proves this for the Euclidean metric
  • Missing from Mizar for the square metric topology equivalent to the product topology
• Definition. Let \(J\) be an indexing set, let \(\mathbf{x}=(x_{\alpha})_{\alpha\in J}\) and \(\mathbf{y}=(y_{\alpha})_{\alpha\in J}\) be points of \(\mathbb{R}^{J}\). We define a metric \(\bar{\rho}\) on \(\mathbb{R}^{J}\) by \(\bar{\rho}(\mathbf{x},\mathbf{y})=\sup\{\bar{d}(x_{\alpha},y_{\alpha})\mid\alpha\in J\}\) where \(\bar{d}\) is the standard bounded metric on \(\mathbb{R}\). This is called the Uniform Metric on \(\mathbb{R}^{J}\) and it induces the Uniform Topology on \(\mathbb{R}^{J}\).
  • Missing from Mizar — at least, in this particular formulation. I believe that it could be cobbled together using the UNIFORM1, UNIFORM2, and UNIFORM3 articles.
• Theorem 20.4. The uniform topology on \(\mathbb{R}^{J}\) is finer than the product topology but coareser than the box topology. Further, all three topologies are distinct when \(J\) is infinite. Missing from Mizar
• Theorem 20.5. Let \(\bar{d}\) be the standard bounded metric on \(\mathbb{R}\). If \(\mathbf{x}\in\mathbb{R}^{\omega}\) and \(\mathbf{y}\in\mathbb{R}^{\omega}\), define \(D(\mathbf{x},\mathbf{y})=\sup\{\bar{d}(x_{n},y_{n})/n\mid n\in\mathbb{N}\}\). Then \(D\) is a metric on \(\mathbb{R}^{\omega}\) which induces the same topology as the product topology. Missing from Mizar

Several results are said very quickly in passing, without enumerating them within a theorem.

• If \(A\subset X\) is a subset of a metric space, then \(d\) restricts to a metric on \(A\). Missing from Mizar
• Metric spaces are Hausdorff. (PCOMPS_1:34)
• Countable products of metrizable spaces are metrizable. Missing from Mizar
• Theorem 21.1. Let \((X, d_{X})\) and \((Y,d_{Y})\) be metric spaces, let \(f\colon X\to Y\) be a function. Then \(f\) is continuous if and only if for each \(x\in X\) and \(\varepsilon\gt0\) there exists a \(\delta\gt0\) such that for every \(y\in X\) we have \(d_{X}(x,y)\lt\delta\) implies \(d_{Y}(f(x),f(y))\lt\varepsilon\). Missing from Mizar

• Lemma 21.2. Let \((X,\mathcal{T})\) be a topological space, let \(A\subset X\) be a subset. If there is a sequence of points \((x_{n})\) of \(A\) converging to \(x\), then \(x\in\operatorname{Cl}(A)\). (FRECHET2:13)

  If \((X,\mathcal{T})\) is metrizable and \(x\in\operatorname{Cl}(A)\), then there exists a sequence of points \((x_{n})\) entirely in \(A\) which converges \(x_{n}\to x\). Missing from Mizar

• Theorem 21.3. Let \((X,\mathcal{T}_{X})\) and \((Y,\mathcal{T}_{Y})\) be topological spaces, let \(f\colon X\to Y\). If \(f\) is continuous, then every convergent sequence \(x_{n}\to x\) in \(X\) maps to a convergent sequence \(f(x_{n})\to f(x)\) in \(Y\). (FRECHET2:12)

  If \(X\) is metrizable and \(y_{n}\to y\) is a convergent sequence of points in \(Y\), then there exists a sequence \(x_{n}\to x\) of points of \(X\) such that \(f(x_{n})=y_{n}\) and \(f(x)=y\). Missing from Mizar

• Lemma 21.4. Addition, subtraction, and multiplication are continuous functions \(\mathbb{R}\times\mathbb{R}\to\mathbb{R}\) and division is a continuous function of \(\mathbb{R}\times(\mathbb{R}\setminus\{0\})\to\mathbb{R}\).
  • This follows immediately from the definition of an AffineMap (FCONT_1:def 4) which is registered as continuous; division is probably "obviously" determined to be continuous, using the identity map being continuous and using later results
• Definition. Let \((X,\mathcal{T})\) be a topological space. We call \(X\) First-Countable if it has a countable basis at each of its points. (FRECHET:def 2)
• Theorem 21.5. Let \((X,\mathcal{T})\) be a topological space, let \(f,g\colon X\to\mathbb{R}\) be continuous functions. Then the functions \(f+g\), \(f-g\), \(fg\) defined by pointwise addition, subtraction, and multiplication are all continuous functions; further, if \(g(x)\neq0\) for every \(x\in X\), then \(f/g\) defined by pointwise division is continuous. (Registered in TOPREALC and TOPREALC)
• Definition. Let \((X,\mathcal{T})\) be a topological space and \((Y,d)\) be a metric space, let \(f_{n}\colon X\to Y\) be a sequence of functions. We say \((f_{n})\) Converges Uniformly to the function \(f\colon X\to Y\) if for each \(\varepsilon\gt0\) there exists a positive integer \(N\) such that \(d(f_{n}(x),f(x))\lt\varepsilon\) for any \(n\gt N\) and \(x\in X\).
  • This seems to be a generalization idiosyncratic to Munkres; Mizar defines is_uniformly_convergent_to in MESFUN9C:def 5 for real-valued functions on an arbitrary set \(X\). So I'm going to say this is kind-of Missing from Mizar
• Theorem 21.6. Let \((X,\mathcal{T})\) be a topological space and \((Y,d)\) be a metric space, let \(f_{n}\colon X\to Y\) be a sequence of functions. If \((f_{n})\) converges uniformly to \(f\), then \(f\) is continuous. Missing from Mizar

This is so highly idiosyncratic to Munkres, and I dislike his presentation of the material. The only place where quotient topological spaces seem to even be tangentially related to the material formalized is in the article T_1TOPSP.

• Definition. Let \((X,\mathcal{T})\) be a topological space. A Separation of \(X\) is a pair \(U\), \(V\) of disjoint nonempty open subsets of \(X\) whose union is \(X\). (CONNSP_1:3)

  The space \(X\) is called Connected if there does not exist a separation of \(X\).

  • Mizar allows \(U\) and/or \(V\) to be empty sets in a separation
  • CONNSP_1:def 2 says \(X\) is connected if it has a separation \(U\), \(V\) with \(V=\emptyset\).
• Theorem 23.3. The union of a collection of connected subspaces of \(X\) that have a point in common are connected. (CONNSP_1:26)
• Theorem 23.4. Let \(A\) be a connected subspace of \(X\), let \(B\) be a subspace of \(X\). If \(A\subset X\subset\operatorname{Cl}(A)\), then \(B\) is connected. (CONNSP_1:18)
• Theorem 23.5. The image of a connected space under a continuous map is connected. (CONNSP_1:14)
• Theorem 23.6. The product of finitely many connected spaces is a connected space. Missing from Mizar

• Definition. A simply-ordered set \(L\) having more than one element is called a Linear Continuum if
  1. \(L\) has the least upper bound property and
  2. if \(x\lt y\), there exists a \(z\in L\) such that \(x\lt z\) and \(z\lt y\).
• The notion of a "linear continuum" seems to be idiosyncratic to Munkres, hence it is Missing from Mizar
• Theorem 24.1. If \(L\) is a linear continuum in the order topology, then \(L\) is connected and so are intervals are rays in \(L\). Missing from Mizar
• Corollary 24.2. The real line \(\mathbb{R}\) is connected and so are intervals and rays in \(\mathbb{R}\).
  • BORSUK_5:77 proves closed intervals are connected and registers that R^1 is pathwise-connected
• Definition. Let \((X,\mathcal{T})\) be a topological space, let \(x,y\in X\). Then a Path in \(X\) connecting \(x\) and \(y\) is a continuous function \(f\colon[a,b]\to X\) such that \(f(a)=x\) and \(f(b)=y\) (and \(a\lt b\)).
  • BORSUK_2:def 2 defines a path as a continuous function \(f\colon[0,1]\to X\) with \(f(0)=x\) and \(f(1)=y\).
• Definition. Let \((X,\mathcal{T})\) be a topological space. We say \(X\) is Path Connected if every pair of points can be connected by a path.
  • BORSUK_2:def 3 gives the definition for pathwise connected using BORSUK_2:def 1
• Example: Unit ball
• Example: unit sphere as a subset of the topological vector space \(\mathbb{R}^{n}\) is defined in TOPREAL9:def 3

• Definition. A collection \(\mathcal{A}\) of subsets of a space \((X,\mathcal{T})\) is said to Cover \(X\) if \(\bigcup\mathcal{A}=X\).

  When every element of \(\mathcal{A}\) is an open subset of \(X\), then we call \(\mathcal{A}\) an Open Cover of \(X\).

  • SETFAM_1:def 11 defines a Cover of X, and Theorem SETFAM_1:45 establishes this logical equivalence
• Definition. Let \((X,\mathcal{T})\) be a topological space. We say \(X\) is Compact if every open cover of \(X\) has a finite subcover. (COMPTS_1:def 1)
  • We can extend this notion to any subset \(A\) of \(X\), which is done in Definition COMPTS_1:def 4.
• Lemma 26.1. Let \(Y\) be a subspace of \((X,\mathcal{T})\). Then \(Y\) is compact if and only if every covering \(Y\) by open subsets of \(X\) contains a finite subcover.
  • (COMPTS_1:2) appears to prove the claim
• Theorem 26.2. Every closed subspace of a compact space is compact. (COMPTS_1:8)
• Theorem 26.3. Every compact subspace of a Hausdorff space is closed. (COMPTS_1:7)
• Theorem 26.4. If \(Y\) is a compact subspace of a Hausdorff space \(X\) and \(x_{0}\in X\) but \(x_{0}\notin Y\), then there exists disjoint open subsets \(U,V\subset X\) such that \(x_{0}\in U\) and \(Y\subset V\). (COMPTS_1:6)
• Theorem 26.5. The image of a compact space under a continuous mapping is compact. (COMPTS_1:15)
• Theorem 26.6. Let \(f\colon X\to Y\) be a bijective continuous function. If \(X\) is compact and \(Y\) is Hausdorff, then \(f\) is a homeomorphism. (COMPTS_1:17)
• Theorem 26.7. The product of finitely many compact spaces is compact.
  • Mizar proves a stronger theorem: the product of arbitrarily many compact spaces is compact. (YELLOW17:23)
• Definition. Let \((X,\mathcal{T})\) be a topological space. A collection \(\mathcal{C}\) of subsets of \(X\) is said to have the Finite Intersection Property if every finite subcollection \(\{C_{1},\dots,C_{n}\}\) has a nonempty intersection \(C_{1}\cap\cdots\cap C_{n}\neq\emptyset\).
  • FINSET_1:def 3 calls this centered
• Theorem 26.9. Let \((X,\mathcal{T})\) be a topological space. Then \(X\) is compact if and only if every collection \(\mathcal{C}\) of closed sets in \(X\) having the finite intersection property we have the intersection of elements of \(\mathcal{C}\) be nonempty \(\bigcap\mathcal{C}\neq\emptyset\). (COMPTS_1:4)

• Theorem 27.1. Let \(X\) be a simply ordered set having the least upper bound property. In the order topology, each closed inteval of \(X\) is compact. Missing from Mizar
• Corollary 27.2. Closed intervals of \(\mathbb{R}\) are compact. (HEINE:4)
• Theorem 27.3. A subspace \(A\) of \(\mathbb{R}^{n}\) is compact if and only if it is closed and bounded in the Euclidean metric \(d\) or square metric \(\rho\). Missing from Mizar
• Theorem 27.4 (Extreme value theorem). Let \(f\colon X\to Y\) be a continuous function, let \(Y\) be an ordered set in the order topology. If \(X\) is compact, then there exist points \(c,d\in X\) such that every point \(x\in X\) satisfies \(f(c)\leq f(x)\leq f(d)\). Missing from Mizar
• Definition. Let \((X,d)\) be a metric space, let \(A\subset X\) be non-empty. For each \(x\in X\), we define the Distance from \(x\) to \(A\) by the equation \(d(x,A)=\inf\{d(x,a)\mid a\in A\}\).
  • I think WEIERSTR:def 6 formalizes this notion, we'd write (dist_min A).x instead of \(d(x,A)\).

• Lemma 27.5 (Lebesgue Number Theorem). Let \(\mathcal{A}\) be an open covering of the metric space \((X,d)\). If \(X\) is compact, there is a \(\delta\gt0\) such taht for each subset of \(X\) having diameter less than \(\delta\), there exists an element of \(\mathcal{A}\) covering it.

  The number \(\delta\) is called a Lebesgue number for the covering \(\mathcal{A}\).

  • UNIFORM1:6 formalizes the theorem, the notion of a Lebesgue number is implicit.
• Definition. A function of metric spaces \(f\colon(X,d_{X})\to(Y,d_{Y})\) is called Uniformly Continuous if for each \(\varepsilon\gt0\) there is a \(\delta\gt0\) such that for every \(x_{0},x_{1}\in X\) we have \(d_{X}(x_{0},x_{1})\lt\delta\) implies \(d_{Y}(f(x_{0}),f(x_{1}))\lt\varepsilon\). (UNIFORM1:def 1)
• Theorem 27.6 (Uniform continuity theorem). Let \(f\colon X\to Y\) be a continuous map of metric spaces. Then \(f\) is uniformly continuous. (UNIFORM1:7)
• Definition. Let \((X,\mathcal{T})\) be a space, \(x_{0}\in X\) is called an Isolated Point of \(X\) if \(\{x_{0}\}\) is open. (TOPGEN1:23)
• Theorem 27.7. Nonempty Hausdorff spaces with no isolated points are uncountable. Missing from Mizar

• Definition. If a space \((X,\mathcal{T})\) has a countable basis for its topology, then we say it is Secound-Countable. (WAYBEL23:def 6)
• Theorem 30.2. A subspace of a second-countable space is second-countable. The Cartesian product of countably many second-countable spaces is second-countable.
  • METRIZTS registers the direct product \(X\times Y\) of second-countable spaces is second-countable
  • METRIZTS registers subspaces of a second-countable space is second-countable
• Definition. Let \((X,\mathcal{T})\) be a topological space, let \(A\subset X\) be a subset. We say \(A\) is Dense in \(X\) if \(\operatorname{Cl}(A)=X\). (TOPS_1:def 3)
• Definition. A space is called Lindelof if every open covering contains a countable subcover. (METRIZTS:def 2)
• Theorem 30.3. Suppose \((X,\mathcal{T})\) is second-countable.
  1. Every open covering of \(X\) contains a countable subcovering, i.e., \(X\) is Lindelof. (METRIZTS registers this fact.)
  2. There exists a countable subset of \(X\) that is dense in \(X\) (TOPGEN_4:6 and TOPGEN_4:7 imply this result)
• Definition. A space is called Separable if it has a countably dense subset. (TOPGEN_1:def 13)

• Definition. Let \((X,\mathcal{T})\) be a topological space where every one-point subset of \(X\) is closed.
  1. We call \(X\) Regular if any point \(x_{0}\) and closed subset \(B\subset X\) not containing \(x_{0}\notin B\), there exists open sets \(U\), \(V\) containing \(x_{0}\in U\) and \(B\subset V\) which are disjoint \(U\cap V=\emptyset\). (PRE_TOPC:def 11)
  2. We call \(X\) Normal if every pair of disjoint closed subsets \(A\), \(B\) of \(X\) are contained in disjoint open subsets of \(X\). (PRE_TOPC:def 12).
• Lemma 31.1. Let \((X,\mathcal{T})\) be a topological space where every one-point subset of \(X\) is closed. Then:
  1. \(X\) is regular if and only if for every point \(x\in X\) and open subset \(U\subset X\) which contains \(x\in U\), there exists a \(V\subset X\) open such that \(x\in V\) and \(\operatorname{Cl}(V)\subset U\). (URYSOHN1:21)
  2. \(X\) is normal if and only if for every subset \(A\subset X\) closed and every \(U\subset X\) open, \(A\subset U\) implies there is an open \(V\subset X\) such that \(A\subset V\) and \(\operatorname{Cl}(V)\subset U\). (CONNSP_2:20)
• Theorem 31.2. We have the following results:
  1. Subspaces of Hausdorff spaces are Hausdorff. (TOPMETR:2)
  2. Products of Hausdorff spaces are Hausdorff. Missing from Mizar
  3. A subspace of regular spaces is regular. Missing from Mizar
  4. Products of regular spaces is regular. Missing from Mizar

• Lemma 32.1. Every regular space with a countable basis is normal.
  • You only need regular and Lindelof to be normal, and it's registered in METRIZTS
• Theorem 32.2. Every metrizable space is normal. (NAGATA_1:15)
• Theorem 32.3. Compact Hausdorff spaces are normal. (COMPTS_1:13)
• Theorem 32.4. Well-ordered sets equipped with the order topology is normal. Missing from Mizar

• Theorem 33.1 (Urysohn Lemma). Let \((X,\mathcal{T})\) be a normal space, let \(A\) and \(B\) be closed subsets of \(X\). Let \([a,b]\) be a closed interval in the real line. Then there exists a continuous map \(f\colon X\to[a,b]\) such that (i) \(f(x)=a\) for all \(x\in A\), and (ii) \(f(x)=b\) for all \(x\in B\). (URYSOHN3:20)
• Definition. Let \((X,\mathcal{T})\) be a topological space; let \(A\) and \(B\) be subsets of \(X\). If there exists a continuous function \(f\colon X\to[0,1]\) such that \(f(A)=\{0\}\) and \(f(B)=\{1\}\), then we say \(A\) and \(B\) can be separated by a continuous function. Missing from Mizar
• Definition. Let \((X,\mathcal{T})\) be a topological space. We say \(X\) is Completely Regular if one-point sets are closed in \(X\) and if for each \(x\in X\) and closed subsets \(A\subset X\) not containing \(x\notin A\), there exists a continuous \(f\colon X\to[0,1]\) such that \(f(x_{0})=1\) and \(f(A)=\{0\}\).
  • Mizar uses the term Tychonoff and it is defined in TOPGEN_5:def 4.
• Theorem 33.2. Subspaces of countably regular spaces are completely regular. Products of completely regular spaces are completely regular. Missing from Mizar

• Theorem 34.1 (Urysohn Metrization Theorem). Every regular space with a countable basis is metrizable. Missing from Mizar

• Theorem 34.2 (Embedding theorem). Let \((X,\mathcal{T})\) be a space where all singletons are closed. Suppose \(\{f_{\alpha}\}_{\alpha\in J}\) is a family of continuous functions \(f_{\alpha}\colon X\to\mathbb{R}\) satisfying the requirement that each point \(x_{0}\in X\) and each open set \(U\subset X\) containing \(x_{0}\in U\), there is an index \(\alpha\in J\) such that \(f_{\alpha}\) is positive at \(x_{0}\) and vanishes outside \(U\).

  Then the function \(F\colon X\to\mathbb{R}^{J}\) defined by \(F(x)=(f_{\alpha}(x))_{\alpha\in J}\) is an embedding of \(X\) in \(\mathbb{R}^{J}\). If \(f_{\alpha}\) maps \(X\) onto the interval \([0,1]\) for each \(\alpha\), then \(F\) embeds \(X\) into \([0,1]^{J}\). Missing from Mizar

• Theorem 34.3. A space \((X,\mathcal{T})\) is completely regular if and only if it is homeomorphic to \([0,1]^{J}\) for some \(J\). Missing from Mizar

• Theorem 35.1 (Tietze extension theorem). Let \((X,\mathcal{T})\) be a normal space and \(A\) be a closed subspace of \(X\).
  1. Any continuous map of \(A\) into the closed interval \([a,b]\) of \(\mathbb{R}\) may be extended to a continuous map of all of \(X\) into \([a,b]\). (TIETZE:23)
  2. Any continuous map of \(A\) into \(\mathbb{R}\) may be extended to a continuous map of all \(X\) into \(\mathbb{R}\). Missing from Mizar

• Definition. Let \((X,\mathcal{T})\) ba a topological space, let \(\mathcal{A}\) be a collection of subsets of \(X\). We say \(\mathcal{A}\) is Locally Finite in \(X\) if every point of \(X\) has a neighborhood that intersects only finitely many elements of \(\mathcal{A}\). (PCOMPS_1:def 1)
• Lemma 39.1. Let \(\mathcal{A}\) be a locally finite collection of subsets of \((X,\mathcal{T})\). Then:
  1. Any subcollection of \(\mathcal{A}\) is locally finite (PCOMPS_1:9)
  2. The collection \(\mathcal{B}=\{\operatorname{Cl}(A)\}_{A\in\mathcal{A}}\) of the closures of the elements of \(\mathcal{A}\) is locally finite. (PCOMPS_1:18 where clf is introduced to form the family \(\mathcal{B}\) from \(\mathcal{A}\))
  3. \(\operatorname{Cl}(\bigcup_{A\in\mathcal{A}}A)=\bigcup_{A\in\mathcal{A}}\operatorname{Cl}(A)\) (PCOMPS_1:20)
• Definition. A collection \(\mathcal{B}\) of subsets of \(X\) is said to be Countably Locally Finite if \(\mathcal{B}\) can be written as the countable union of collections \(\mathcal{B}_{n}\) each of which is locally finite. Missing from Mizar
• Definition. Let \(\mathcal{A}\) be a collection of subsets of the space \((X,\mathcal{T})\). A collection \(\mathcal{B}\) of subsets of \(X\) is said to be a Refinement of \(\mathcal{A}\) if for each \(B\in\mathcal{B}\) there exists a \(A\in\mathcal{A}\) containing \(B\subset A\).
  • This is the same as is_finer_than for collections of sets
• Lemma 39.2. Let \((X,\mathcal{T})\) be a metrizable space. If \(\mathcal{A}\) is an open covering of \(X\), then there is an open covering \(\mathcal{E}\) of \(X\) refining \(\mathcal{A}\) that is countably locally finite. (PCOMPS_2:6)

• Definition. A subset \(A\) of a space \((X,\mathcal{T})\) is called a \(G_{\delta}\) set in \(X\) if it is equal to the intersection of a countable collection of open subsets of \(X\). Missing from Mizar
• Lemma 40.1. Let \((X,\mathcal{T})\) be a regular space with basis \(\mathcal{B}\) that is countably locally finite. Then \(X\) is normal and every closed set in \(X\) is a \(G_{\delta}\) set in \(X\).
  • NAGATA_1:20 proves \(X\) is normal
  • The proposition that "…every closed set in \(X\) is a \(G_{\delta}\) set in \(X\)" Missing from Mizar
• Lemma 40.2. Let \((X,\mathcal{T})\) be normal, let \(A\) be a closed \(G_{\delta}\) set in \(X\). Then there is a continuous function \(f\colon X\to[0,1]\) such that \(f(x)=0\) for \(x\in A\) and \(f(x)\gt0\) for \(x\notin A\). Missing from Mizar
• Theorem 40.3 (Nagata-Smirnov metrization theorem). A space \((X,\mathcal{T})\) is metrizable if and only if \((X,\mathcal{T})\) is regular and has a basis that is countably locally finite. (NAGATA_2:19)
  • Mizar uses the attribute Basis_sigma_locally_finite to formalize that second condition "has a basis that is countably locally finite".

• Definition. A space \((X,\mathcal{T})\) is called Paracompact if every open covering \(\mathcal{A}\) of \(X\) has a finite open refinement \(\mathcal{B}\) that covers \(X\). (PCOMPS_1:def 3)
• Theorem 41.1. Every paracompact Hausdorff space is normal. (PCOMPS_1:25)
• Theorem 41.2. Every closed subspace of a paracompact space is paracompact.
• Lemma 41.3. Let \((X,\mathcal{T})\) be regular. Then the following conditions on \(X\) are equivalent: Every open covering of \(X\) has a refinement that is:
  1. An open covering of \(X\) and countably locally finite Missing from Mizar
  2. An covering of \(X\) and locally finite Missing from Mizar
  3. A closed covering of \(X\) and locally finite Missing from Mizar
  4. An open covering of \(X\) and locally finite Missing from Mizar
• Theorem 41.4. Every metrizable space is paracompact. (PCOMPS_2:7)
• Theorem 41.5. Every regular Lindelof space is paracompact. Missing from Mizar