(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2019 Slawomir Kolodynski This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹ Uniform spaces › theory UniformSpace_ZF imports Topology_ZF_2 Topology_ZF_4a begin text‹ This theory defines uniform spaces and proves their basic properties. › subsection‹ Definition and motivation › text‹ Just like a topological space constitutes the minimal setting in which one can speak of continuous functions, the notion of uniform spaces (commonly attributed to André Weil) captures the minimal setting in which one can speak of uniformly continuous functions. In some sense this is a generalization of the notion of metric (or metrizable) spaces and topological groups. › text‹ There are several definitions of uniform spaces. The fact that these definitions are equivalent is far from obvious (some people call such phenomenon cryptomorphism). We will use the definition of the uniform structure (or ''uniformity'') based on entourages. This was the original definition by Weil and it seems to be the most commonly used. A uniformity consists of entourages that are binary relations between points of space $X$ that satisfy a certain collection of conditions, specified below. › definition IsUniformity ("_ {is a uniformity on} _" 90) where "Φ {is a uniformity on} X ≡(Φ {is a filter on} (X×X)) ∧ (∀U∈Φ. id(X) ⊆ U ∧ (∃V∈Φ. V O V ⊆ U) ∧ converse(U) ∈ Φ)" text‹ If $\Phi$ is a uniformity on $X$, then the every element $V$ of $\Phi$ is a certain relation on $X$ (a subset of $X\times X$) and is called an ''entourage''. For an $x\in X$ we call $V\{ x\}$ a neighborhood of $x$. The first useful fact we will show is that neighborhoods are non-empty. › lemma neigh_not_empty: assumes "Φ {is a uniformity on} X" "W∈Φ" and "x∈X" shows "W``{x} ≠ 0" and "x ∈ W``{x}" proof - from assms(1,2) have "id(X) ⊆ W" unfolding IsUniformity_def IsFilter_def by auto with ‹x∈X› show" x∈W``{x}" and "W``{x} ≠ 0" by auto qed text‹The filter part of the definition of uniformity for easier reference:› lemma unif_filter: assumes "Φ {is a uniformity on} X" shows "Φ {is a filter on} (X×X)" using assms unfolding IsUniformity_def by simp text‹The second part of the definition of uniformity for easy reference:› lemma entourage_props: assumes "Φ {is a uniformity on} X" and "A∈Φ" shows "A ⊆ X×X" "id(X) ⊆ A" "∃V∈Φ. V O V ⊆ A" "converse(A) ∈ Φ" proof - from assms show "id(X) ⊆ A" "∃V∈Φ. V O V ⊆ A" "converse(A) ∈ Φ" unfolding IsUniformity_def by auto from assms show "A ⊆ X×X" using unif_filter unfolding IsFilter_def by blast qed text‹The definition of uniformity states (among other things) that for every member $U$ of uniformity $\Phi$ there is another one, say $V$ such that $V\circ V\subseteq U$. Sometimes such $V$ is said to be half the size of $U$. The next lemma states that $V$ can be taken to be symmetric. › lemma half_size_symm: assumes "Φ {is a uniformity on} X" "W∈Φ" shows "∃V∈Φ. V O V ⊆ W ∧ V=converse(V)" proof - from assms obtain U where "U∈Φ" and "U O U ⊆ W" unfolding IsUniformity_def by auto let ?V = "U ∩ converse(U)" from assms(1) ‹U∈Φ› have "?V ∈ Φ" and "?V = converse(?V)" unfolding IsUniformity_def IsFilter_def by auto moreover from ‹U O U ⊆ W› have "?V O ?V ⊆ W" by auto ultimately show ?thesis by blast qed text‹Inside every member $W$ of the uniformity $\Phi$ we can find one that is symmetric and smaller than a third of size $W$. Compare with the Metamath's theorem with the same name.› lemma ustex3sym: assumes "Φ {is a uniformity on} X" "A∈Φ" shows "∃B∈Φ. B O (B O B) ⊆ A ∧ B=converse(B)" proof - from assms obtain C where "C∈Φ" and "C O C ⊆ A" unfolding IsUniformity_def by auto from assms(1) ‹C∈Φ› obtain B where "B∈Φ" "B O B ⊆ C" and "B=converse(B)" using half_size_symm by blast with ‹C O C ⊆ A› have "(B O B) O (B O B) ⊆ A" by blast with assms(1) ‹B∈Φ› have "B O (B O B) ⊆ A" using entourage_props(1,2) by blast with ‹B∈Φ› ‹B=converse(B)› show ?thesis by blast qed text‹If $\Phi$ is a uniformity on $X$ then every element of $\Phi$ is a subset of $X\times X$ whose domain is $X$. › lemma uni_domain: assumes "Φ {is a uniformity on} X" "W∈Φ" shows "W ⊆ X×X" and "domain(W) = X" proof - from assms show "W ⊆ X×X" unfolding IsUniformity_def IsFilter_def by blast show "domain(W) = X" proof from assms show "domain(W) ⊆ X" unfolding IsUniformity_def IsFilter_def by auto from assms show "X ⊆ domain(W)" unfolding IsUniformity_def by blast qed qed text‹If $\Phi$ is a uniformity on $X$ and $W\in \Phi$ the for every $x\in X$ the image of the singleton $\{ x\}$ by $W$ is contained in $X$. Compare the Metamath's theorem with the same name. › lemma ustimasn: assumes "Φ {is a uniformity on} X" "W∈Φ" and "x∈X" shows "W``{x} ⊆ X" using assms uni_domain(1) by auto text‹ Uniformity ‹Φ› defines a natural topology on its space $X$ via the neighborhood system that assigns the collection $\{V(\{x\}):V\in \Phi\}$ to every point $x\in X$. In the next lemma we show that if we define a function this way the values of that function are what they should be. This is only a technical fact which is useful to shorten the remaining proofs, usually treated as obvious in standard mathematics. › lemma neigh_filt_fun: assumes "Φ {is a uniformity on} X" defines "ℳ ≡ {⟨x,{V``{x}.V∈Φ}⟩.x∈X}" shows "ℳ:X→Pow(Pow(X))" and "∀x∈X. ℳ`(x) = {V``{x}.V∈Φ}" proof - from assms have "∀x∈X. {V``{x}.V∈Φ} ∈ Pow(Pow(X))" using IsUniformity_def IsFilter_def image_subset by auto with assms show "ℳ:X→Pow(Pow(X))" using ZF_fun_from_total by simp with assms show "∀x∈X. ℳ`(x) = {V``{x}.V∈Φ}" using ZF_fun_from_tot_val by simp qed text‹ In the next lemma we show that the collection defined in lemma ‹neigh_filt_fun› is a filter on $X$. The proof is kind of long, but it just checks that all filter conditions hold.› lemma filter_from_uniformity: assumes "Φ {is a uniformity on} X" and "x∈X" defines "ℳ ≡ {⟨x,{V``{x}.V∈Φ}⟩.x∈X}" shows "ℳ`(x) {is a filter on} X" proof - from assms have PhiFilter: "Φ {is a filter on} (X×X)" and "ℳ:X→Pow(Pow(X))" and "ℳ`(x) = {V``{x}.V∈Φ}" using IsUniformity_def neigh_filt_fun by auto have "0 ∉ ℳ`(x)" proof - from assms ‹x∈X› have "0 ∉ {V``{x}.V∈Φ}" using neigh_not_empty by blast with ‹ℳ`(x) = {V``{x}.V∈Φ}› show "0 ∉ ℳ`(x)" by simp qed moreover have "X ∈ ℳ`(x)" proof - note ‹ℳ`(x) = {V``{x}.V∈Φ}› moreover from assms have "X×X ∈ Φ" unfolding IsUniformity_def IsFilter_def by blast hence "(X×X)``{x} ∈ {V``{x}.V∈Φ}" by auto moreover from ‹x∈X› have "(X×X)``{x} = X" by auto ultimately show "X ∈ ℳ`(x)" by simp qed moreover from ‹ℳ:X→Pow(Pow(X))› ‹x∈X› have "ℳ`(x) ⊆ Pow(X)" using apply_funtype by blast moreover have LargerIn: "∀B ∈ ℳ`(x). ∀C ∈ Pow(X). B⊆C ⟶ C ∈ ℳ`(x)" proof - { fix B assume "B ∈ ℳ`(x)" fix C assume "C ∈ Pow(X)" and "B⊆C" from ‹ℳ`(x) = {V``{x}.V∈Φ}› ‹B ∈ ℳ`(x)› obtain U where "U∈Φ" and "B = U``{x}" by auto let ?V = "U ∪ C×C" from assms ‹U∈Φ› ‹C ∈ Pow(X)› have "?V ∈ Pow(X×X)" and "U⊆?V" using IsUniformity_def IsFilter_def by auto with ‹U∈Φ› PhiFilter have "?V∈Φ" using IsFilter_def by simp moreover from assms ‹U∈Φ› ‹x∈X› ‹B = U``{x}› ‹B⊆C› have "C = ?V``{x}" using neigh_not_empty image_greater_rel by simp ultimately have "C ∈ {V``{x}.V∈Φ}" by auto with ‹ℳ`(x) = {V``{x}.V∈Φ}› have "C ∈ ℳ`(x)" by simp } thus ?thesis by blast qed moreover have "∀A ∈ ℳ`(x).∀B ∈ ℳ`(x). A∩B ∈ ℳ`(x)" proof - { fix A B assume "A ∈ ℳ`(x)" and "B ∈ ℳ`(x)" with ‹ℳ`(x) = {V``{x}.V∈Φ}› obtain V⇩_{A}V⇩_{B}where "A = V⇩_{A}``{x}" "B = V⇩_{B}``{x}" and "V⇩_{A}∈ Φ" "V⇩_{B}∈ Φ" by auto let ?C = "V⇩_{A}``{x} ∩ V⇩_{B}``{x}" from assms ‹V⇩_{A}∈ Φ› ‹V⇩_{B}∈ Φ› have "V⇩_{A}∩V⇩_{B}∈ Φ" using IsUniformity_def IsFilter_def by simp with ‹ℳ`(x) = {V``{x}.V∈Φ}› have "(V⇩_{A}∩V⇩_{B})``{x} ∈ ℳ`(x)" by auto moreover from PhiFilter ‹V⇩_{A}∈ Φ› ‹V⇩_{B}∈ Φ› have "?C ∈ Pow(X)" unfolding IsFilter_def by auto moreover have "(V⇩_{A}∩V⇩_{B})``{x} ⊆ ?C" using image_Int_subset_left by simp moreover note LargerIn ultimately have "?C ∈ ℳ`(x)" by simp with ‹A = V⇩_{A}``{x}› ‹B = V⇩_{B}``{x}› have "A∩B ∈ ℳ`(x)" by blast } thus ?thesis by simp qed ultimately show ?thesis unfolding IsFilter_def by simp qed text‹A rephrasing of ‹filter_from_uniformity›: if $\Phi$ is a uniformity on $X$, then $\{V(\{ x\}) | V\in \Phi\}$ is a filter on $X$ for every $x\in X$.› lemma unif_filter_at_point: assumes "Φ {is a uniformity on} X" and "x∈X" shows "{V``{x}.V∈Φ} {is a filter on} X" using assms filter_from_uniformity ZF_fun_from_tot_val1 by simp text‹A frequently used property of filters is that they are "upward closed" i.e. supersets of a filter element are also in the filter. The next lemma makes this explicit for easy reference as applied to the natural filter created from a uniformity.› corollary unif_filter_up_closed: assumes "Φ {is a uniformity on} X" "x∈X" "U ∈ {V``{x}. V∈Φ}" "W⊆X" "U⊆W" shows "W ∈ {V``{x}.V∈Φ}" using assms filter_from_uniformity ZF_fun_from_tot_val1 unfolding IsFilter_def by auto text‹ The function defined in the premises of lemma ‹neigh_filt_fun› (or ‹filter_from_uniformity›) is a neighborhood system. The proof uses the existence of the "half-the-size" neighborhood condition (‹∃V∈Φ. V O V ⊆ U›) of the uniformity definition, but not the ‹converse(U) ∈ Φ› part. › theorem neigh_from_uniformity: assumes "Φ {is a uniformity on} X" shows "{⟨x,{V``{x}.V∈Φ}⟩.x∈X} {is a neighborhood system on} X" proof - let ?ℳ = "{⟨x,{V``{x}.V∈Φ}⟩.x∈X}" from assms have "?ℳ:X→Pow(Pow(X))" and Mval: "∀x∈X. ?ℳ`(x) = {V``{x}.V∈Φ}" using IsUniformity_def neigh_filt_fun by auto moreover from assms have "∀x∈X. (?ℳ`(x) {is a filter on} X)" using filter_from_uniformity by simp moreover { fix x assume "x∈X" have "∀N∈?ℳ`(x). x∈N ∧ (∃U∈?ℳ`(x).∀y∈U.(N∈?ℳ`(y)))" proof - { fix N assume "N∈?ℳ`(x)" have "x∈N" and "∃U∈?ℳ`(x).∀y∈U.(N ∈ ?ℳ`(y))" proof - from ‹?ℳ:X→Pow(Pow(X))› Mval ‹x∈X› ‹N∈?ℳ`(x)› obtain U where "U∈Φ" and "N = U``{x}" by auto with assms ‹x∈X› show "x∈N" using neigh_not_empty by simp from assms ‹U∈Φ› obtain V where "V∈Φ" and "V O V ⊆ U" unfolding IsUniformity_def by auto let ?W = "V``{x}" from ‹V∈Φ› Mval ‹x∈X› have "?W ∈ ?ℳ`(x)" by auto moreover have "∀y∈?W. N ∈ ?ℳ`(y)" proof - { fix y assume "y∈?W" with ‹?ℳ:X→Pow(Pow(X))› ‹x∈X› ‹?W ∈ ?ℳ`(x)› have "y∈X" using apply_funtype by blast with assms have "?ℳ`(y) {is a filter on} X" using filter_from_uniformity by simp moreover from assms ‹y∈X› ‹V∈Φ› have "V``{y} ∈ ?ℳ`(y)" using neigh_filt_fun by auto moreover from ‹?ℳ:X→Pow(Pow(X))› ‹x∈X› ‹N ∈ ?ℳ`(x)› have "N ∈ Pow(X)" using apply_funtype by blast moreover from ‹V O V ⊆ U› ‹y∈?W› have "V``{y} ⊆ (V O V)``{x}" and "(V O V)``{x} ⊆ U``{x}" by auto with ‹N = U``{x}› have "V``{y} ⊆ N" by blast ultimately have "N ∈ ?ℳ`(y)" unfolding IsFilter_def by simp } thus ?thesis by simp qed ultimately show "∃U∈?ℳ`(x).∀y∈U.(N ∈ ?ℳ`(y))" by auto qed } thus ?thesis by simp qed } ultimately show ?thesis unfolding IsNeighSystem_def by simp qed text‹ When we have a uniformity $\Phi$ on $X$ we can define a topology on $X$ in a (relatively) natural way. We will call that topology the ‹ UniformTopology(Φ)›. We could probably reformulate the definition to skip the $X$ parameter because if $\Phi$ is a uniformity on $X$ then $X$ can be recovered from (is determined by) $\Phi$. › definition "UniformTopology(Φ,X) ≡ {U∈Pow(X). ∀x∈U. U∈{V``{x}. V∈Φ}}" text‹An identity showing how the definition of uniform topology is constructed. Here, the $M = \{\langle t,\{ V\{ t\} : V\in \Phi\}\rangle : t\in X\}$ is the neighborhood system (a function on $X$) created from uniformity $\Phi$. Then for each $x\in X$, $M(x) = \{ V\{ t\} : V\in \Phi\}$ is the set of neighborhoods of $x$. › lemma uniftop_def_alt: shows "UniformTopology(Φ,X) = {U ∈ Pow(X). ∀x∈U. U ∈ {⟨t,{V``{t}.V∈Φ}⟩.t∈X}`(x)}" proof - let ?ℳ = "{⟨x,{V``{x}. V∈Φ}⟩. x∈X}" have "∀U∈Pow(X).∀x∈U. ?ℳ`(x) = {V``{x}. V∈Φ}" using ZF_fun_from_tot_val1 by auto then show ?thesis unfolding UniformTopology_def by auto qed text‹ The collection of sets constructed in the ‹ UniformTopology › definition is indeed a topology on $X$. › theorem uniform_top_is_top: assumes "Φ {is a uniformity on} X" shows "UniformTopology(Φ,X) {is a topology}" and "⋃ UniformTopology(Φ,X) = X" using assms neigh_from_uniformity uniftop_def_alt topology_from_neighs by auto text‹If we have a uniformity $\Phi$ we can create a neighborhood system from it in two ways. We can create a a neighborhood system directly from $\Phi$ using the formula $X \ni x \mapsto \{V\{x\} | x\in X\}$ (see theorem ‹neigh_from_uniformity›). Alternatively we can construct a topology from $\Phi$ as in theorem ‹uniform_top_is_top› and then create a neighborhood system from this topology as in theorem ‹neigh_from_topology›. The next theorem states that these two ways give the same result. › theorem neigh_unif_same: assumes "Φ {is a uniformity on} X" shows "{⟨x,{V``{x}.V∈Φ}⟩. x∈X} = {neighborhood system of} UniformTopology(Φ,X)" using assms neigh_from_uniformity nei_top_nei_round_trip uniftop_def_alt by simp text‹Another form of the definition of topology generated from a uniformity.› lemma uniftop_def_alt1: assumes "Φ {is a uniformity on} X" shows "UniformTopology(Φ,X) = {U∈Pow(X). ∀x∈U. ∃W∈Φ. W``{x} ⊆ U}" proof let ?T = "UniformTopology(Φ,X)" show "?T ⊆ {U∈Pow(X). ∀x∈U. ∃W∈Φ. W``{x} ⊆ U}" unfolding UniformTopology_def by auto { fix U assume "U∈{U∈Pow(X). ∀x∈U. ∃W∈Φ. W``{x} ⊆ U}" then have "U∈Pow(X)" and I: "∀x∈U. ∃W∈Φ. W``{x} ⊆ U" by auto { fix x assume "x∈U" with I obtain W where "W∈Φ" and "W``{x} ⊆ U" by auto let ?𝔉 = "{V``{x}.V∈Φ}" from assms(1) ‹U∈Pow(X)› ‹x∈U› ‹W∈Φ› have "?𝔉 {is a filter on} X" and "W``{x} ∈ ?𝔉" using unif_filter_at_point by auto with ‹U∈Pow(X)› ‹W``{x} ⊆ U› have "U∈?𝔉" using is_filter_def_split(5) by blast } hence "∀x∈U. U ∈ {V``{x}.V∈Φ}" by simp with ‹U∈Pow(X)› have "U∈?T" unfolding UniformTopology_def by simp } thus "{U∈Pow(X). ∀x∈U. ∃W∈Φ. W``{x} ⊆ U} ⊆ ?T" by blast qed text‹Images of singletons by entourages are neighborhoods of those singletons.› lemma image_singleton_ent_nei: assumes "Φ {is a uniformity on} X" "V∈Φ" "x∈X" defines "ℳ ≡ {neighborhood system of} UniformTopology(Φ,X)" shows "V``{x} ∈ ℳ`(x)" proof - from assms(1,4) have "ℳ = {⟨x,{V``{x}.V∈Φ}⟩. x∈X}" using neigh_unif_same by simp with assms(2,3) show ?thesis using ZF_fun_from_tot_val1 by auto qed text‹The set neighborhoods of a singleton $\{ x\}$ where $x\in X$ consist of images of the singleton by the entourages $W\in \Phi$. See also the Metamath's theorem with the same name. › lemma utopsnneip: assumes "Φ {is a uniformity on} X" "x∈X" defines "𝒮 ≡ {set neighborhood system of} UniformTopology(Φ,X)" shows "𝒮`{x} = {W``{x}. W∈Φ}" proof - let ?T = "UniformTopology(Φ,X)" let ?ℳ = "{neighborhood system of} ?T" from assms(1,2) have "x ∈ ⋃?T" using uniform_top_is_top(2) by simp with assms(3) have "?ℳ`(x) = 𝒮`{x}" using neigh_from_nei by simp moreover from assms(1) have "?ℳ = {⟨x,{W``{x}.W∈Φ}⟩. x∈X}" using neigh_unif_same by simp with assms(2) have "?ℳ`(x) = {W``{x}.W∈Φ}" using ZF_fun_from_tot_val1 by simp ultimately show ?thesis by simp qed text‹Images of singletons by entourages are set neighborhoods of those singletons. See also the Metamath theorem with the same name.› corollary utopsnnei: assumes "Φ {is a uniformity on} X" "W∈Φ" "x∈X" defines "𝒮 ≡ {set neighborhood system of} UniformTopology(Φ,X)" shows "W``{x} ∈ 𝒮`{x}" using assms utopsnneip by auto text‹If $\Phi$ is a uniformity on $X$ that generates a topology $T$, $R$ is any relation on $X$ (i.e. $R\subseteq X\times X$), $W$ is a symmetric entourage (i.e. $W\in \Phi$, and $W$ is symmetric (i.e. equal to its converse)), then the closure of $R$ in the product topology is contained the the composition $V\circ (M \circ V)$. Metamath has a similar theorem with the same name. › lemma utop3cls: assumes "Φ {is a uniformity on} X" "R⊆X×X" "W∈Φ" "W=converse(W)" defines "J ≡ UniformTopology(Φ,X)" shows "Closure(R,J×⇩_{t}J) ⊆ W O (R O W)" proof let ?M = "{set neighborhood system of} (J×⇩_{t}J)" fix z assume zMem: "z ∈ Closure(R,J×⇩_{t}J)" from assms(1,5) have Jtop: "J {is a topology}" and "⋃J = X" using uniform_top_is_top by auto then have JJtop: "(J×⇩_{t}J) {is a topology}" and JxJ: "⋃(J×⇩_{t}J) = X×X" using Top_1_4_T1(1,3) by auto with assms(2) have "topology0(J×⇩_{t}J)" and "R ⊆ ⋃(J×⇩_{t}J)" unfolding topology0_def by auto then have "Closure(R,J×⇩_{t}J) ⊆ ⋃(J×⇩_{t}J)" using topology0.Top_3_L11(1) by simp with ‹z ∈ Closure(R,J×⇩_{t}J)› JxJ have "z∈X×X" by auto let ?x = "fst(z)" let ?y = "snd(z)" from ‹z∈X×X› have "?x∈X" "?y∈X" "z = ⟨?x,?y⟩" by auto with assms(1,3,5) Jtop have "(W``{?x})×(W``{?y}) ∈ ?M`({?x}×{?y})" using utopsnnei neitx by simp moreover from ‹z = ⟨?x,?y⟩› have "{?x}×{?y} = {z}" by (rule pair_prod) ultimately have "(W``{?x})×(W``{?y}) ∈ ?M`{z}" by simp with zMem JJtop ‹R ⊆ ⋃(J×⇩_{t}J)› have "(W``{?x})×(W``{?y}) ∩ R ≠ 0" using neindisj by blast with assms(4) have "⟨?x,?y⟩ ∈ W O (R O W)" using sym_rel_comp by simp with ‹z = ⟨?x,?y⟩› show "z ∈ W O (R O W)" by simp qed text‹Uniform spaces are regular ($T_3$). › theorem utopreg: assumes "Φ {is a uniformity on} X" shows "UniformTopology(Φ,X) {is regular}" proof - let ?J = "UniformTopology(Φ,X)" let ?𝒮 = "{set neighborhood system of} ?J" from assms have "⋃?J = X" and Jtop: "?J {is a topology}" and cntx: "topology0(?J)" using uniform_top_is_top unfolding topology0_def by auto have "∀U∈?J. ∀x∈U. ∃V∈?J. x∈V ∧ Closure(V,?J)⊆U" proof - { fix U x assume "U∈?J" "x∈U" then have "U ∈ ?𝒮`{x}" using open_nei_singl by simp from ‹U∈?J› have "U⊆⋃?J" by auto with ‹x∈U› ‹⋃?J = X› have "x∈X" by auto from assms(1) ‹x∈X› ‹U ∈ ?𝒮`{x}› obtain A where "U=A``{x}" and "A∈Φ" using utopsnneip by auto from assms(1) ‹A∈Φ› obtain W where "W∈Φ" "W O (W O W) ⊆ A" and Wsymm: "W=converse(W)" using ustex3sym by blast with assms(1) ‹x∈X› have "W``{x} ∈ ?𝒮`{x}" and "W``{x} ⊆ X" using utopsnnei ustimasn by auto from ‹W``{x} ∈ ?𝒮`{x}› have "∃V∈?J. {x}⊆V ∧ V⊆W``{x}" by (rule neii2) then obtain V where "V∈?J" "x∈V" "V⊆W``{x}" by blast have "Closure(V,?J) ⊆ U" proof - from assms(1) ‹W∈Φ› ‹⋃?J = X› have "W ⊆ X×X" using entourage_props(1) by simp from cntx ‹W``{x} ⊆ X› ‹⋃?J = X› ‹V⊆W``{x}› have "Closure(V,?J) ⊆ Closure(W``{x},?J)" using topology0.top_closure_mono by simp also have "Closure(W``{x},?J) ⊆ Closure(W,?J×⇩_{t}?J)``{x}" proof - from ‹W⊆X×X› ‹x∈X› ‹⋃?J = X› have "W⊆(⋃?J)×(⋃?J)" "x∈⋃?J" by auto with ‹?J {is a topology}› show ?thesis using imasncls by simp qed also from assms(1) ‹W⊆X×X› ‹W∈Φ› Wsymm ‹W O (W O W) ⊆ A› have "Closure(W,?J×⇩_{t}?J)``{x} ⊆ A``{x}" using utop3cls by blast finally have "Closure(V,?J) ⊆ A``{x}" by simp with ‹U=A``{x}› show ?thesis by auto qed with ‹V∈?J› ‹x∈V› have "∃V∈?J. x∈V ∧ Closure(V,?J)⊆U" by blast } thus ?thesis by simp qed with Jtop show "?J {is regular}" using is_regular_def_alt by simp qed end