(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2020 Daniel de la Concepcion 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 ‹Topological groups - uniformity› theory TopologicalGroup_Uniformity_ZF imports TopologicalGroup_ZF UniformSpace_ZF_1 begin text‹ Each topological group is a uniform space. This theory is about the unifomities that are naturally defined by a topological group structure. › subsection‹Natural uniformities in topological groups: definitions and notation› text‹There are two basic uniformities that can be defined on a topological group. › text‹Definition of left uniformity› definition (in topgroup) leftUniformity where "leftUniformity ≡ {V∈Pow(G×G).∃U∈ 𝒩⇩_{0}. {⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈U} ⊆ V}" text‹Definition of right uniformity› definition (in topgroup) rightUniformity where "rightUniformity ≡ {V∈Pow(G×G).∃U∈ 𝒩⇩_{0}. {⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈U}⊆ V}" text‹Right and left uniformities are indeed uniformities. › lemma (in topgroup) side_uniformities: shows "leftUniformity {is a uniformity on} G" and "rightUniformity {is a uniformity on} G" proof- { assume "0 ∈ leftUniformity" then obtain U where U:"U∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈U}⊆0" unfolding leftUniformity_def by auto have "⟨𝟬,𝟬⟩:G×G" using zero_in_tgroup by auto moreover have "(\<rm>𝟬)\<ra>𝟬 = 𝟬" using group0_valid_in_tgroup group0.group_inv_of_one group0.group0_2_L2 zero_in_tgroup by auto moreover have "𝟬∈int(U)" using U(1) by auto then have "𝟬∈U" using Top_2_L1 by auto ultimately have "⟨𝟬,𝟬⟩∈{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈U}" by auto with U(2) have "⟨𝟬,𝟬⟩∈0" by blast hence False by auto } hence "0∉leftUniformity" by auto moreover have "leftUniformity ⊆ Pow(G×G)" unfolding leftUniformity_def by auto moreover { have "G×G∈Pow(G×G)" by auto moreover have "{⟨s,t⟩:G×G. (\<rm>s)\<ra>t:G} ⊆ G×G" by auto moreover note zneigh_not_empty ultimately have "G×G∈leftUniformity" unfolding leftUniformity_def by auto } moreover { fix A B assume as:"A∈leftUniformity" "B∈leftUniformity" from as(1) obtain AU where AU:"AU∈ 𝒩⇩_{0}" "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈AU}⊆ A" "A∈Pow(G×G)" unfolding leftUniformity_def by auto from as(2) obtain BU where BU:"BU∈ 𝒩⇩_{0}" "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈BU}⊆ B" "B∈Pow(G×G)" unfolding leftUniformity_def by auto from AU(1) BU(1) have "𝟬∈int(AU)∩int(BU)" by auto moreover from AU BU have op:"int(AU)∩int(BU)∈T" using Top_2_L2 topSpaceAssum IsATopology_def by auto moreover have "int(AU)∩int(BU) ⊆ AU∩BU" using Top_2_L1 by auto with op have "int(AU)∩int(BU)⊆int(AU∩BU)" using Top_2_L5 by auto moreover note AU(1) BU(1) ultimately have "AU∩BU: 𝒩⇩_{0}" unfolding zerohoods_def by auto moreover have "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈AU∩BU}⊆{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈AU}" by auto with AU(2) BU(2) have "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈AU∩BU}⊆A∩B" by auto ultimately have "A∩B ∈ {V∈Pow(G×G).∃U∈ 𝒩⇩_{0}. {⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈U} ⊆ V}" using AU(3) BU(3) by blast then have "A∩B∈leftUniformity" unfolding leftUniformity_def by simp } hence "∀A∈leftUniformity. ∀B∈leftUniformity. A ∩ B ∈ leftUniformity" by auto moreover { fix B C assume as:"B∈leftUniformity" "C∈Pow(G × G)" "B ⊆ C" from as(1) obtain BU where BU:"BU∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ BU}⊆B" unfolding leftUniformity_def by blast from as(3) BU(2) have "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ BU}⊆C" by auto with as(2) BU(1) have "C ∈ {V∈Pow(G×G).∃U∈ 𝒩⇩_{0}. {⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈U} ⊆ V}" by auto then have "C ∈ leftUniformity" unfolding leftUniformity_def by auto } then have "∀B∈leftUniformity. ∀C∈Pow(G×G). B⊆C ⟶ C∈leftUniformity" by auto ultimately have leftFilter:"leftUniformity {is a filter on} (G×G)" unfolding IsFilter_def by auto { assume "0∈rightUniformity" then obtain U where U:"U∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈U}⊆0" unfolding rightUniformity_def by auto have "⟨𝟬,𝟬⟩:G×G" using zero_in_tgroup by auto moreover have "𝟬\<ra>(\<rm>𝟬) = 𝟬" using group0_valid_in_tgroup group0.group_inv_of_one group0.group0_2_L2 zero_in_tgroup by auto moreover have "𝟬∈int(U)" using U(1) by auto then have "𝟬∈U" using Top_2_L1 by auto ultimately have "⟨𝟬,𝟬⟩∈{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈U}" by auto with U(2) have "⟨𝟬,𝟬⟩∈0" by blast hence False by auto } then have "0∉rightUniformity" by auto moreover have "rightUniformity ⊆ Pow(G×G)" unfolding rightUniformity_def by auto moreover { have "G×G∈Pow(G×G)" by auto moreover have "{⟨s,t⟩:G×G. (\<rm>s)\<ra>t:G} ⊆ G×G" by auto moreover note zneigh_not_empty ultimately have "G×G ∈ rightUniformity" unfolding rightUniformity_def by auto } moreover { fix A B assume as:"A∈rightUniformity" "B∈rightUniformity" from as(1) obtain AU where AU:"AU∈ 𝒩⇩_{0}" "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈AU}⊆ A" "A∈Pow(G×G)" unfolding rightUniformity_def by auto from as(2) obtain BU where BU:"BU∈ 𝒩⇩_{0}" "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈BU}⊆ B" "B∈Pow(G×G)" unfolding rightUniformity_def by auto from AU(1) BU(1) have "𝟬∈int(AU)∩int(BU)" by auto moreover from AU BU have op:"int(AU)∩int(BU)∈T" using Top_2_L2 topSpaceAssum IsATopology_def by auto moreover have "int(AU)∩int(BU) ⊆ AU∩BU" using Top_2_L1 by auto with op have "int(AU)∩int(BU)⊆int(AU∩BU)" using Top_2_L5 by auto moreover note AU(1) BU(1) ultimately have "AU∩BU: 𝒩⇩_{0}" unfolding zerohoods_def by auto moreover have "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈AU∩BU}⊆{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈AU}" by auto with AU(2) BU(2) have "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈AU∩BU}⊆A∩B" by auto ultimately have "A∩B ∈ {V∈Pow(G×G).∃U∈ 𝒩⇩_{0}. {⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈U}⊆ V}" using AU(3) BU(3) by blast then have "A∩B ∈ rightUniformity" unfolding rightUniformity_def by simp } hence "∀A∈rightUniformity. ∀B∈rightUniformity. A∩B ∈ rightUniformity" by auto moreover { fix B C assume as:"B∈rightUniformity" "C∈Pow(G × G)" "B ⊆ C" from as(1) obtain BU where BU:"BU∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ BU}⊆B" unfolding rightUniformity_def by blast from as(3) BU(2) have "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ BU}⊆C" by auto then have "C ∈ rightUniformity" using as(2) BU(1) unfolding rightUniformity_def by auto } then have "∀B∈rightUniformity. ∀C∈Pow(G×G). B⊆C ⟶ C∈rightUniformity" by auto ultimately have rightFilter:"rightUniformity {is a filter on} (G×G)" unfolding IsFilter_def by auto { fix U assume as:"U∈leftUniformity" from as obtain V where V:"V∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ V} ⊆ U" unfolding leftUniformity_def by auto then have "V⊆G" by auto { fix x assume as2:"x∈id(G)" from as obtain V where V:"V∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ V} ⊆ U" unfolding leftUniformity_def by auto from V(1) have "𝟬∈int(V)" by auto then have V0:"𝟬∈V" using Top_2_L1 by auto from as2 obtain t where t:"x=⟨t,t⟩" "t:G" by auto from t(2) have "(\<rm>t)\<ra>t =𝟬" using group0_valid_in_tgroup group0.group0_2_L6 by auto with V0 t V(2) have "x∈U" by auto } then have "id(G)⊆U" by auto moreover { { fix x assume ass:"x∈{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ \<sm>V}" then obtain s t where as:"s∈G" "t∈G" "(\<rm>s)\<ra>t ∈ \<sm>V" "x=⟨s,t⟩" by force from as(3) ‹V⊆G› have "(\<rm>s)\<ra>t∈{\<rm>q. q∈V}" using ginv_image_add by simp then obtain q where q: "q∈V" "(\<rm>s)\<ra>t = \<rm>q" by auto with ‹V⊆G› have "q∈G" by auto with ‹s∈G› ‹t∈G› ‹(\<rm>s)\<ra>t = \<rm>q› have "q=(\<rm>t)\<ra>s" using simple_equation1_add by blast with q(1) have "(\<rm>t)\<ra>s ∈ V" by auto with as(1,2) have "⟨t,s⟩ ∈ U" using V(2) by auto then have "⟨s,t⟩ ∈ converse(U)" by auto with as(4) have "x ∈ converse(U)" by auto } then have "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ \<sm>V} ⊆ converse(U)" by auto moreover have "(\<sm>V):𝒩⇩_{0}" using neg_neigh_neigh V(1) by auto moreover note as ultimately have "converse(U) ∈ leftUniformity" unfolding leftUniformity_def by auto } moreover { from V(1) obtain W where W:"W:𝒩⇩_{0}" "W \<sad> W ⊆V" using exists_procls_zerohood by blast { fix x assume as:"x ∈ {⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ W} O {⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ W}" then obtain x⇩_{1}x⇩_{2}x⇩_{3}where x:"x⇩_{1}∈G" "x⇩_{2}∈G" "x⇩_{3}∈G" "(\<rm>x⇩_{1})\<ra>x⇩_{2}∈ W" "(\<rm>x⇩_{2})\<ra>x⇩_{3}∈ W" "x=⟨x⇩_{1},x⇩_{3}⟩" unfolding comp_def by auto from W(1) have "W\<sad>W = f``(W×W)" using interval_add(2) by auto moreover from W(1) have WW:"W×W⊆G×G" by auto moreover from x(4,5) have "⟨(\<rm>x⇩_{1})\<ra>x⇩_{2},(\<rm>x⇩_{2})\<ra>x⇩_{3}⟩:W×W" by auto with WW have "f`(⟨(\<rm>x⇩_{1})\<ra>x⇩_{2},(\<rm>x⇩_{2})\<ra>x⇩_{3}⟩):f``(W×W)" using func_imagedef topgroup_f_binop by auto ultimately have "((\<rm>x⇩_{1})\<ra>x⇩_{2})\<ra>((\<rm>x⇩_{2})\<ra>x⇩_{3}) :W\<sad>W" by auto moreover from x(1,2,3) have "((\<rm>x⇩_{1})\<ra>x⇩_{2})\<ra>((\<rm>x⇩_{2})\<ra>x⇩_{3}) = (\<rm>x⇩_{1})\<ra> x⇩_{3}" using cancel_middle_add(2) by simp ultimately have "(\<rm>x⇩_{1})\<ra> x⇩_{3}∈W\<sad>W" by auto with W(2) have "(\<rm>x⇩_{1})\<ra> x⇩_{3}∈V" by auto with x(1,3,6) have "x:{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ V}" by auto } then have "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ W} O {⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ W} ⊆ U" using V(2) by auto moreover have "{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ W}∈leftUniformity" unfolding leftUniformity_def using W(1) by auto ultimately have "∃Z∈leftUniformity. Z O Z⊆U" by auto } ultimately have "id(G)⊆U ∧ (∃Z∈leftUniformity. Z O Z⊆U) ∧ converse(U)∈leftUniformity" by blast } then have "∀U∈leftUniformity. id(G)⊆U ∧ (∃Z∈leftUniformity. Z O Z⊆U) ∧ converse(U)∈leftUniformity" by auto with leftFilter show "leftUniformity {is a uniformity on} G" unfolding IsUniformity_def by auto { fix U assume as:"U∈rightUniformity" from as obtain V where V:"V∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ V} ⊆ U" unfolding rightUniformity_def by auto { fix x assume as2:"x∈id(G)" from as obtain V where V:"V∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ V} ⊆ U" unfolding rightUniformity_def by auto from V(1) have "𝟬∈int(V)" by auto then have V0:"𝟬∈V" using Top_2_L1 by auto from as2 obtain t where t:"x=⟨t,t⟩" "t:G" by auto from t(2) have "t\<ra>(\<rm>t) =𝟬" using group0_valid_in_tgroup group0.group0_2_L6 by auto with V0 t V(2) have "x∈U" by auto } then have "id(G)⊆U" by auto moreover { { fix x assume ass:"x∈{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ \<sm>V}" then obtain s t where as:"s∈G" "t∈G" "s\<ra>(\<rm>t) ∈ \<sm>V" "x=⟨s,t⟩" by force from as(3) V(1) have "s\<ra>(\<rm>t) ∈ {\<rm>q. q∈V}" using ginv_image_add by simp then obtain q where q:"q∈V" "s\<ra>(\<rm>t) = \<rm>q" by auto with ‹V∈𝒩⇩_{0}› have "q∈G" by auto with as(1,2) q(1,2) have "t\<ra>(\<rm>s) ∈ V" using simple_equation0_add by blast with as(1,2,4) V(2) have "x ∈ converse(U)" by auto } then have "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ \<sm>V} ⊆ converse(U)" by auto moreover from V(1) have "(\<sm>V) ∈ 𝒩⇩_{0}" using neg_neigh_neigh by auto ultimately have "converse(U) ∈ rightUniformity" using as rightUniformity_def by auto } moreover { from V(1) obtain W where W:"W:𝒩⇩_{0}" "W \<sad> W ⊆V" using exists_procls_zerohood by blast { fix x assume as:"x:{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ W} O {⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ W}" then obtain x⇩_{1}x⇩_{2}x⇩_{3}where x:"x⇩_{1}:G" "x⇩_{2}∈G" "x⇩_{3}∈G" "x⇩_{1}\<ra>(\<rm>x⇩_{2}) ∈ W" "x⇩_{2}\<ra>(\<rm>x⇩_{3}) ∈ W" "x=⟨x⇩_{1},x⇩_{3}⟩" unfolding comp_def by auto from W(1) have "W\<sad>W = f``(W×W)" using interval_add(2) by auto moreover from W(1) have WW:"W×W⊆G×G" by auto moreover from x(4,5) have "⟨x⇩_{1}\<ra>(\<rm>x⇩_{2}),x⇩_{2}\<ra>(\<rm>x⇩_{3})⟩ ∈ W×W" by auto with WW have "f`(⟨x⇩_{1}\<ra>(\<rm>x⇩_{2}),x⇩_{2}\<ra>(\<rm>x⇩_{3})⟩) ∈ f``(W×W)" using func_imagedef topgroup_f_binop by auto ultimately have "(x⇩_{1}\<ra>(\<rm>x⇩_{2}))\<ra>(x⇩_{2}\<ra>(\<rm>x⇩_{3})) ∈ W\<sad>W" by auto moreover from x(1,2,3) have "(x⇩_{1}\<ra>(\<rm>x⇩_{2}))\<ra>(x⇩_{2}\<ra>(\<rm>x⇩_{3})) = x⇩_{1}\<ra> (\<rm>x⇩_{3})" using cancel_middle_add(1) by simp ultimately have "x⇩_{1}\<ra>(\<rm>x⇩_{3}) ∈ W\<sad>W" by auto with W(2) have "x⇩_{1}\<ra>(\<rm>x⇩_{3}) ∈ V" by auto then have "x ∈ {⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ V}" using x(1,3,6) by auto } with V(2) have "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ W} O {⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ W} ⊆ U" by auto moreover from W(1) have "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t) ∈ W} ∈ rightUniformity" unfolding rightUniformity_def by auto ultimately have "∃Z∈rightUniformity. Z O Z⊆U" by auto } ultimately have "id(G)⊆U ∧ (∃Z∈rightUniformity. Z O Z⊆U) ∧ converse(U)∈rightUniformity" by blast } then have "∀U∈rightUniformity. id(G)⊆U ∧ (∃Z∈rightUniformity. Z O Z⊆U) ∧ converse(U)∈rightUniformity" by auto with rightFilter show "rightUniformity {is a uniformity on} G" unfolding IsUniformity_def by auto qed text‹ The topologies generated by the right and left uniformities are the original group topology. › lemma (in topgroup) top_generated_side_uniformities: shows "UniformTopology(leftUniformity,G) = T" and "UniformTopology(rightUniformity,G) = T" proof- let ?M = "{⟨t, {V `` {t} . V ∈ leftUniformity}⟩. t∈G}" have fun:"?M:G→Pow(Pow(G))" using neigh_from_uniformity side_uniformities(1) IsNeighSystem_def by auto let ?N = "{⟨t, {V `` {t} . V ∈ rightUniformity}⟩. t∈G}" have funN:"?N:G→Pow(Pow(G))" using neigh_from_uniformity side_uniformities(2) IsNeighSystem_def by auto { fix U assume op:"U∈T" hence "U⊆G" by auto { fix x assume x:"x∈U" with op have xg:"x∈G" and "(\<rm>x) ∈ G" using neg_in_tgroup by auto then have "⟨x, {V``{x}. V ∈ leftUniformity}⟩ ∈ {⟨t, {V``{t}. V ∈ leftUniformity}⟩. t∈G}" by auto with fun have app:"?M`(x) = {V``{x}. V ∈ leftUniformity}" using ZF_fun_from_tot_val by auto have "(\<rm>x)\<ltr>U : 𝒩⇩_{0}" using open_trans_neigh op x by auto then have V:"{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t∈((\<rm>x)\<ltr>U)} ∈ leftUniformity" unfolding leftUniformity_def by auto with xg have N:"∀t∈G. t:{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t∈((\<rm>x)\<ltr>U)}``{x} ⟷ (\<rm>x)\<ra>t∈((\<rm>x)\<ltr>U)" using image_iff by auto { fix t assume t:"t∈G" { assume as:"(\<rm>x)\<ra>t∈((\<rm>x)\<ltr>U)" then have "(\<rm>x)\<ra>t∈LeftTranslation(G,f,\<rm>x)``U" by auto then obtain q where q:"q∈U" "⟨q,(\<rm>x)\<ra>t⟩∈LeftTranslation(G,f,\<rm>x)" using image_iff by auto with op have "q∈G" by auto from q(2) have "(\<rm>x)\<ra>q = (\<rm>x)\<ra>t" unfolding LeftTranslation_def by auto with ‹(\<rm>x) ∈ G› ‹q∈G› ‹t∈G› have "q = t" using neg_in_tgroup cancel_left_add by blast with q(1) have "t∈U" by auto } moreover { assume t:"t∈U" with ‹U⊆G› ‹(\<rm>x)∈G› have "(\<rm>x)\<ra>t ∈ ((\<rm>x)\<ltr>U)" using lrtrans_image(1) by auto } ultimately have "(\<rm>x)\<ra>t∈((\<rm>x)\<ltr>U) ⟷ t:U" by blast } with N have "∀t∈G. t:{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t ∈ ((\<rm>x)\<ltr>U)}``{x} ⟷ t∈U" by blast with op have "∀t. t:{⟨s,t⟩∈G×G. (\<rm>s)\<ra>t∈((\<rm>x)\<ltr>U)}``{x} ⟷ t:U" by auto hence "U = {⟨s,t⟩∈G×G. (\<rm>s)\<ra>t∈((\<rm>x)\<ltr>U)}``{x}" by auto with V have "∃V∈leftUniformity. U=V``{x}" by blast with app have "U ∈ {⟨t, {V `` {t} . V ∈ leftUniformity}⟩ . t ∈ G}`(x)" by auto moreover from ‹x∈G› funN have app:"?N`(x) = {V``{x}. V ∈ rightUniformity}" using ZF_fun_from_tot_val by simp moreover from x op have openTrans:"U\<rtr>(\<rm>x): 𝒩⇩_{0}" using open_trans_neigh_2 by auto then have V:"{⟨s,t⟩∈G×G. s\<ra>(\<rm>t)∈(U\<rtr>(\<rm>x))} ∈ rightUniformity" unfolding rightUniformity_def by auto with xg have N:"∀t∈G. t:{⟨s,t⟩∈G×G. s\<ra>(\<rm>t)∈(U\<rtr>(\<rm>x))}-``{x} ⟷ t\<ra>(\<rm>x)∈(U\<rtr>(\<rm>x))" using vimage_iff by auto moreover { fix t assume t:"t∈G" { assume as:"t\<ra>(\<rm>x)∈(U\<rtr>(\<rm>x))" hence "t\<ra>(\<rm>x)∈RightTranslation(G,f,\<rm>x)``U" by auto then obtain q where q:"q∈U" "⟨q,t\<ra>(\<rm>x)⟩∈RightTranslation(G,f,\<rm>x)" using image_iff by auto with op have "q∈G" by auto from q(2) have "q\<ra>(\<rm>x) = t\<ra>(\<rm>x)" unfolding RightTranslation_def by auto with ‹q∈G› ‹(\<rm>x) ∈ G› ‹t∈G› have "q = t" using cancel_right_add by simp with q(1) have "t∈U" by auto } moreover { assume "t∈U" with ‹(\<rm>x)∈G› ‹U⊆G› have "t\<ra>(\<rm>x)∈(U\<rtr>(\<rm>x))" using lrtrans_image(2) by auto } ultimately have "t\<ra>(\<rm>x)∈(U\<rtr>(\<rm>x)) ⟷ t:U" by blast } with N have "∀t∈G. t:{⟨s,t⟩∈G×G. s\<ra>(\<rm>t)∈(U\<rtr>(\<rm>x))}-``{x} ⟷ t:U" by blast with op have "∀t. t:{⟨s,t⟩∈G×G. s\<ra>(\<rm>t)∈(U\<rtr>(\<rm>x))}-``{x} ⟷ t:U" by auto hence "{⟨s,t⟩∈G×G. s\<ra>(\<rm>t)∈(U\<rtr>(\<rm>x))}-``{x} = U" by auto then have "U = converse({⟨s,t⟩∈G×G. s\<ra>(\<rm>t)∈(U\<rtr>(\<rm>x))})``{x}" unfolding vimage_def by simp with V app have "U ∈ {⟨t, {V `` {t} . V ∈ rightUniformity}⟩ . t ∈ G}`(x)" using side_uniformities(2) IsUniformity_def by auto ultimately have "U ∈ {⟨t, {V `` {t} . V ∈ leftUniformity}⟩ . t ∈ G}`(x)" and "U ∈ {⟨t, {V `` {t} . V ∈ rightUniformity}⟩ . t ∈ G}`(x)" by auto } hence "∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ leftUniformity}⟩ . t ∈ G} ` x" and "∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ rightUniformity}⟩ . t ∈ G} ` x" by auto } hence "T⊆{U ∈ Pow(G) . ∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ leftUniformity}⟩ . t ∈ G} ` x}" and "T⊆{U ∈ Pow(G) . ∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ rightUniformity}⟩ . t ∈ G} ` x}" by auto moreover { fix U assume as:"U ∈ Pow(G)" "∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ leftUniformity}⟩ . t ∈ G}`(x)" { fix x assume x:"x∈U" with as(1) have xg:"x∈G" by auto from x as(2) have "U∈{⟨t, {V `` {t} . V ∈ leftUniformity}⟩ . t ∈ G}`(x)" by auto with xg fun have "U∈{V `` {x} . V ∈ leftUniformity}" using apply_equality by auto then obtain V where V:"U=V``{x}" "V∈leftUniformity" by auto from V(2) obtain W where W:"W∈ 𝒩⇩_{0}" "{⟨s,t⟩:G×G. (\<rm>s)\<ra>t:W}⊆V" unfolding leftUniformity_def by auto from W(2) have A:"{⟨s,t⟩:G×G. (\<rm>s)\<ra>t:W}``{x}⊆V``{x}" by auto from xg have "∀q∈G. q∈({⟨s,t⟩:G×G. (\<rm>s)\<ra>t:W}``{x}) ⟷ (\<rm>x)\<ra>q:W" using image_iff by auto hence B:"{⟨s,t⟩:G×G. (\<rm>s)\<ra>t:W}``{x} = {t∈G. (\<rm>x)\<ra>t:W}" by auto from W(1) have WG:"W⊆G" by auto { fix t assume t:"t ∈ x\<ltr>W" then have "t ∈ LeftTranslation(G,f,x)``W" by auto then obtain s where s:"s∈W" "⟨s,t⟩∈LeftTranslation(G,f,x)" using image_iff by auto with ‹W⊆G› have "s∈G" by auto from s(2) have "t=x\<ra>s" "t∈G" unfolding LeftTranslation_def by auto with ‹x∈G› ‹s∈G› have "(\<rm>x)\<ra>t = s" using put_on_the_other_side(2) by simp with s(1) have "(\<rm>x)\<ra>t∈W" by auto with ‹t∈G› have "t ∈ {s∈G. (\<rm>x)\<ra>s:W}" by auto } then have "x\<ltr>W ⊆ {t∈G. (\<rm>x)\<ra>t∈W}" by auto with B have "x \<ltr> W ⊆ {⟨s,t⟩ ∈ G × G . (\<rm> s) \<ra> t ∈ W} `` {x}" by auto with A have "x \<ltr> W ⊆ V`` {x}" by blast with V(1) have "x \<ltr> W ⊆ U" by auto then have "int(x \<ltr> W) ⊆ U" using Top_2_L1 by blast moreover from xg W(1) have "x∈int(x \<ltr> W)" using elem_in_int_ltrans(1) by auto moreover have "int(x \<ltr> W)∈T" using Top_2_L2 by auto ultimately have "∃Y∈T. x∈Y ∧ Y⊆U" by auto } then have "U∈T" using open_neigh_open by auto } hence "{U ∈ Pow(G) . ∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ leftUniformity}⟩ . t ∈ G} ` x} ⊆ T" by auto moreover { fix U assume as:"U ∈ Pow(G)" "∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ rightUniformity}⟩ . t ∈ G} ` x" { fix x assume x:"x∈U" with as(1) have xg:"x∈G" by auto from x as(2) have "U∈{⟨t, {V `` {t} . V ∈ rightUniformity}⟩ . t ∈ G} ` x" by auto with xg funN have "U∈{V `` {x} . V ∈ rightUniformity}" using apply_equality by auto then obtain V where V:"U=V``{x}" "V ∈ rightUniformity" by auto then have "converse(V) ∈ rightUniformity" using side_uniformities(2) IsUniformity_def by auto then obtain W where W:"W∈ 𝒩⇩_{0}" "{⟨s,t⟩:G×G. s\<ra>(\<rm>t):W}⊆converse(V)" unfolding rightUniformity_def by auto from W(2) have A:"{⟨s,t⟩:G×G. s\<ra>(\<rm>t):W}-``{x}⊆V``{x}" by auto from xg have "∀q∈G. q∈({⟨s,t⟩:G×G. s\<ra>(\<rm>t):W}-``{x}) ⟷ q\<ra>(\<rm>x):W" using image_iff by auto hence B:"{⟨s,t⟩:G×G. s\<ra>(\<rm>t):W}-``{x} = {t∈G. t\<ra>(\<rm>x):W}" by auto from W(1) have WG:"W⊆G" by auto { fix t assume "t ∈ W\<rtr>x" with ‹x∈G› ‹W⊆G› obtain s where "s∈W" and "t=s\<ra>x" using lrtrans_image(2) by auto with ‹W⊆G› have "s∈G" by auto with ‹x∈G› ‹t=s\<ra>x› have "t∈G" using group_op_closed_add by simp from ‹x∈G› ‹s∈G› ‹t=s\<ra>x› have "t\<ra>(\<rm>x) = s" using put_on_the_other_side by simp with ‹s∈W› ‹t∈G› have "t ∈ {s∈G. s\<ra>(\<rm>x) ∈ W}" by auto } then have "W\<rtr>x ⊆ {t:G. t\<ra>(\<rm>x):W}" by auto with B have "W \<rtr> x ⊆ {⟨s,t⟩ ∈ G × G . s \<ra> (\<rm> t) ∈ W}-``{x}" by auto with A have "W \<rtr> x ⊆ V`` {x}" by blast with V(1) have "W \<rtr> x ⊆ U" by auto then have "int(W \<rtr> x) ⊆ U" using Top_2_L1 by blast moreover from xg W(1) have "x∈int(W \<rtr> x)" using elem_in_int_rtrans(1) by auto moreover have "int(W \<rtr> x)∈T" using Top_2_L2 by auto ultimately have "∃Y∈T. x∈Y ∧ Y⊆U" by auto } then have "U∈T" using open_neigh_open by auto } ultimately have "{U ∈ Pow(G). ∀x∈U. U ∈ {⟨t, {V``{t} . V ∈ leftUniformity}⟩. t ∈ G}`(x)} = T" "{U ∈ Pow(G). ∀x∈U. U ∈ {⟨t, {V``{t} . V ∈ rightUniformity}⟩. t ∈ G}`(x)} = T" by auto then show "UniformTopology(leftUniformity,G) = T" and "UniformTopology(rightUniformity,G) = T" using uniftop_def_alt by auto qed text‹ The side uniformities are called this way because of how they affect left and right translations. In the next lemma we show that left translations are uniformly continuous with respect to the left uniformity. › lemma (in topgroup) left_mult_uniformity: assumes "x∈G" shows "LeftTranslation(G,f,x) {is uniformly continuous between} leftUniformity {and} leftUniformity" proof - let ?P = "ProdFunction(LeftTranslation(G, f, x), LeftTranslation(G, f, x))" from assms have L: "LeftTranslation(G,f,x):G→G" and "leftUniformity {is a uniformity on} G" using group0_5_L1 side_uniformities(1) by auto moreover have "∀V ∈ leftUniformity. ?P-``(V) ∈ leftUniformity" proof - { fix V assume "V ∈ leftUniformity" then obtain U where "U ∈ 𝒩⇩_{0}" and "{⟨s,t⟩ ∈ G × G . (\<rm> s) \<ra> t ∈ U} ⊆ V" unfolding leftUniformity_def by auto with ‹V ∈ leftUniformity› have as:"V ⊆ G × G" "U ∈ 𝒩⇩_{0}" "{⟨s,t⟩ ∈ G × G . (\<rm> s) \<ra> t ∈ U} ⊆ V" unfolding leftUniformity_def by auto { fix z assume z:"z ∈ {⟨s,t⟩ ∈ G × G . (\<rm> s) \<ra> t ∈ U}" then obtain s t where st:"z=⟨s,t⟩" "s∈G" "t∈G" by auto from st(1) z have st2: "(\<rm> s) \<ra> t ∈ U" by auto from assms st have "?P`(z) = ⟨LeftTranslation(G, f, x)`(s), LeftTranslation(G, f, x)`(t)⟩" using prodFunctionApp group0_5_L1(2) by blast with assms st(2,3) have "?P`(z) = ⟨x\<ra>s,x\<ra>t⟩" using group0_5_L2(2) by auto moreover from ‹x∈G› ‹s∈G› ‹t∈G› have "(\<rm> (x\<ra>s)) \<ra> (x\<ra>t) = (\<rm>s)\<ra>t" using cancel_middle_add(3) by simp with st2 have "(\<rm> (x\<ra>s)) \<ra> (x\<ra>t) ∈ U" by auto ultimately have "?P`(z) ∈ {⟨s,t⟩ ∈ G × G . (\<rm> s) \<ra> t ∈ U}" using assms st(2,3) group_op_closed by auto with as(3) have "?P`(z) ∈ V" by force with L z have "z ∈ ?P-``(V)" using prodFunction func1_1_L5A vimage_iff by blast } with as(2) have "∃U∈𝒩⇩_{0}. {⟨s,t⟩ ∈ G × G . (\<rm> s) \<ra> t ∈ U} ⊆ ?P-``(V)" by blast with ‹LeftTranslation(G,f,x):G→G› ‹V ⊆ G × G› have "?P-``(V) ∈ leftUniformity" unfolding leftUniformity_def using prodFunction func1_1_L6A by blast } thus ?thesis by simp qed ultimately show ?thesis using IsUniformlyCont_def by auto qed text‹ Right translations are uniformly continuous with respect to the right uniformity. › lemma (in topgroup) right_mult_uniformity: assumes "x∈G" shows "RightTranslation(G,f,x) {is uniformly continuous between} rightUniformity {and} rightUniformity" proof - let ?P = "ProdFunction(RightTranslation(G, f, x), RightTranslation(G, f, x))" from assms have R: "RightTranslation(G,f,x):G→G" and "rightUniformity {is a uniformity on} G" using group0_5_L1 side_uniformities(2) by auto moreover have "∀V ∈ rightUniformity. ?P-``(V) ∈ rightUniformity" proof - { fix V assume "V ∈ rightUniformity" then obtain U where "U ∈ 𝒩⇩_{0}" and "{⟨s,t⟩ ∈ G × G . s \<ra> (\<rm> t) ∈ U} ⊆ V" unfolding rightUniformity_def by auto with ‹V ∈ rightUniformity› have as:"V ⊆ G × G" "U ∈ 𝒩⇩_{0}" "{⟨s,t⟩ ∈ G × G . s \<ra> (\<rm> t) ∈ U} ⊆ V" unfolding rightUniformity_def by auto { fix z assume z:"z ∈ {⟨s,t⟩ ∈ G × G . s \<ra> (\<rm> t) ∈ U}" then obtain s t where st:"z=⟨s,t⟩" "s∈G" "t∈G" by auto from st(1) z have st2: "s \<ra> (\<rm>t) ∈ U" by auto from assms st have "?P`(z) = ⟨RightTranslation(G, f, x)`(s), RightTranslation(G, f, x)`(t)⟩" using prodFunctionApp group0_5_L1(1) by blast with assms st(2,3) have "?P`(z) = ⟨s\<ra>x,t\<ra>x⟩" using group0_5_L2(1) by auto moreover from ‹x∈G› ‹s∈G› ‹t∈G› have "(s\<ra>x) \<ra> (\<rm>(t\<ra>x)) =s\<ra> (\<rm>t)" using cancel_middle_add(4) by simp with st2 have "(s\<ra>x) \<ra> (\<rm>(t\<ra>x)) ∈ U" by auto ultimately have "?P`(z) ∈ {⟨s,t⟩ ∈ G × G . s \<ra> (\<rm> t) ∈ U}" using assms st(2,3) group_op_closed by auto with as(3) have "?P`(z) ∈ V" by force with R z have "z ∈ ?P-``(V)" using prodFunction func1_1_L5A vimage_iff by blast } with as(2) have "∃U∈𝒩⇩_{0}. {⟨s,t⟩ ∈ G × G . s \<ra> (\<rm> t) ∈ U} ⊆ ?P-``(V)" by blast with ‹RightTranslation(G,f,x):G→G› ‹V ⊆ G × G› have "?P-``(V) ∈ rightUniformity" unfolding rightUniformity_def using prodFunction func1_1_L6A by blast } thus ?thesis by simp qed ultimately show ?thesis using IsUniformlyCont_def by auto qed text‹ The third uniformity important on topological groups is called the uniformity of Roelcke. › definition(in topgroup) roelckeUniformity where "roelckeUniformity ≡ {V∈Pow(G×G). ∃U∈ 𝒩⇩_{0}. {⟨s,t⟩∈G×G. t ∈(U\<rtr>s)\<sad>U}⊆ V}" text‹The Roelcke uniformity is indeed a uniformity on the group. › lemma (in topgroup) roelcke_uniformity: shows "roelckeUniformity {is a uniformity on} G" proof - let ?Φ = "roelckeUniformity" have "∀U ∈ ?Φ. id(G)⊆U ∧ (∃V∈?Φ. V O V ⊆ U) ∧ converse(U) ∈ ?Φ" proof fix U assume U:"U ∈ roelckeUniformity" then obtain V where V:"{⟨s,t⟩∈G×G. t ∈(V\<rtr>s)\<sad>V} ⊆ U" "V∈ 𝒩⇩_{0}" "U:Pow(G×G)" unfolding roelckeUniformity_def by auto from V(2) have VG:"V⊆G" by auto have "id(G) ⊆ U" proof - from V(2) have "𝟬∈int(V)" by auto then have V0:"𝟬∈V" using Top_2_L1 by auto { fix x assume x:"x∈G" with ‹V∈𝒩⇩_{0}› have "x ∈ V\<rtr>x" using elem_in_int_rtrans(1) Top_2_L1 by blast with ‹V⊆G› ‹x∈G› ‹𝟬∈V› have "x\<ra>𝟬 : (V\<rtr>x)\<sad>V" using lrtrans_in_group_add(2) interval_add(4) by auto with ‹x∈G› have "x: (V\<rtr>x)\<sad>V" using group0_2_L2 by auto with ‹x∈G› have "⟨x,x⟩:{⟨s,t⟩∈G×G. t ∈(V\<rtr>s)\<sad>V}" by auto with V(1) have "⟨x,x⟩∈U" by auto } thus "id(G) ⊆ U" by auto qed moreover have "converse(U) ∈ ?Φ" proof - { fix l assume "l ∈ {⟨s,t⟩∈G×G. t ∈((\<sm>V)\<rtr>s)\<sad>(\<sm>V)}" then obtain s t where st:"s∈G" "t∈G" "t ∈((\<sm>V)\<rtr>s)\<sad>(\<sm>V)" "l=⟨s,t⟩" by force from ‹V⊆G› have smG:"(\<sm>V) ⊆ G" using ginv_image_add(1) by simp with ‹s∈G› have VxG:"(\<sm>V)\<rtr>s ⊆ G" using lrtrans_in_group_add(2) by simp from ‹V⊆G› ‹t∈G› have VsG:"V\<rtr>t ⊆ G" using lrtrans_in_group_add(2) by simp from st(3) VxG smG obtain x y where xy:"t = x\<ra>y" "x ∈ (\<sm>V)\<rtr>s" "y∈(\<sm>V)" using elements_in_set_sum by blast from xy(2) smG st(1) obtain z where z:"x = z\<ra>s" "z∈(\<sm>V)" using elements_in_rtrans by blast with ‹y∈(\<sm>V)› ‹(\<sm>V)⊆G› ‹s∈G› ‹t = x\<ra>y› have ts:"(\<rm>z)\<ra>t\<ra>(\<rm>y) = s" using cancel_middle_add(5) by blast { fix u assume "u∈(\<sm>V)" with ‹V⊆G› have "(\<rm>u) ∈ V" using ginv_image_el_add by simp } hence R:"∀u∈(\<sm>V).(\<rm>u) ∈ V" by simp with z(2) xy(3) have zy:"(\<rm>z)∈V" "(\<rm>y)∈V" by auto from zy(1) VG st(2) have "(\<rm>z)\<ra>t : V\<rtr>t" using lrtrans_image(2) by auto with zy(2) VG VsG have "(\<rm>z)\<ra>t\<ra>(\<rm>y) : (V\<rtr>t)\<sad>V" using interval_add(4) by auto with ts have "s:(V\<rtr>t)\<sad>V" by auto with st(1,2) have "⟨s,t⟩ ∈ converse({⟨s,t⟩∈G×G. t ∈(V\<rtr>s)\<sad>V})" using converse_iff by auto with V(1) have "⟨s,t⟩ ∈ converse(U)" by auto with st(4) have "l ∈ converse(U)" by auto } then have "{⟨s,t⟩∈G×G. t ∈((\<sm>V)\<rtr>s)\<sad>(\<sm>V)} ⊆ converse(U)" by auto moreover from V(2) have "(\<sm>V): 𝒩⇩_{0}" using neg_neigh_neigh by auto ultimately have "∃V∈ 𝒩⇩_{0}. {⟨s,t⟩∈G×G. t ∈(V\<rtr>s)\<sad>V} ⊆ converse(U)" by auto moreover from V(3) have "converse(U) ⊆ G×G" unfolding converse_def by auto ultimately show "converse(U) ∈ roelckeUniformity" unfolding roelckeUniformity_def by auto qed moreover have "∃Z∈?Φ. Z O Z ⊆ U" proof - from V(2) obtain W where W:"W∈𝒩⇩_{0}" "W\<sad>W ⊆ V" using exists_procls_zerohood by blast then have WG:"W⊆G" by auto moreover { fix k assume as:"k:{⟨s,t⟩∈G×G. t ∈(W\<rtr>s)\<sad>W} O {⟨s,t⟩∈G×G. t ∈(W\<rtr>s)\<sad>W}" then obtain x⇩_{1}x⇩_{2}x⇩_{3}where x:"x⇩_{1}∈G" "x⇩_{2}∈G" "x⇩_{3}∈G" "x⇩_{2}∈ (W\<rtr>x⇩_{1})\<sad>W" "x⇩_{3}∈ (W\<rtr>x⇩_{2})\<sad>W" "k=⟨x⇩_{1},x⇩_{3}⟩" unfolding comp_def by auto from ‹x⇩_{1}∈G› have VsG:"W\<rtr>x⇩_{1}⊆ G" and Vx1G:"V\<rtr>x⇩_{1}⊆ G" using lrtrans_in_group_add(2) by auto from x(4) VsG WG obtain x y where xy:"x⇩_{2}= x\<ra>y" "x ∈ W\<rtr>x⇩_{1}" "y∈W" using elements_in_set_sum by blast from xy(2) WG x(1) obtain z where z:"x = z\<ra>x⇩_{1}" "z∈W" using elements_in_rtrans by blast from z(2) xy(3) WG have yzG:"y∈G" "z∈G" by auto from x(2) have VsG:"W\<rtr>x⇩_{2}⊆ G" using lrtrans_in_group_add by simp from x(5) VsG WG obtain x' y' where xy2:"x⇩_{3}= x'\<ra>y'" "x'∈ W\<rtr>x⇩_{2}" "y'∈W" using elements_in_set_sum by blast from xy2(2) WG x(2) obtain z' where z2:"x' = z'\<ra>x⇩_{2}" "z'∈W" using elements_in_rtrans by blast from z2(2) xy2(3) WG have yzG2:"y'∈G" "z'∈G" by auto from xy(1) z(1) xy2(1) z2(1) have "x⇩_{3}= (z'\<ra>(z\<ra>x⇩_{1}\<ra>y))\<ra>y'" by auto with yzG yzG2 x(1) have x3:"x⇩_{3}= ((z'\<ra>z)\<ra>x⇩_{1})\<ra>(y\<ra>y')" using group_oper_assoc group_op_closed by simp from xy(3) z(2) xy2(3) z2(2) WG have "z'\<ra>z ∈ W\<sad>W" "y\<ra>y' ∈ W\<sad>W" using interval_add(4) by auto with W(2) have yzV:"z'\<ra>z ∈ V" "y\<ra>y' ∈ V" by auto from yzV(1) VG x(1) have "(z'\<ra>z)\<ra>x⇩_{1}∈ V\<rtr>x⇩_{1}" using lrtrans_image(2) by auto with yzV(2) Vx1G VG have "((z'\<ra>z)\<ra>x⇩_{1})\<ra>(y\<ra>y') ∈ (V\<rtr>x⇩_{1})\<sad>V" using interval_add(4) by auto with x3 have "x⇩_{3}∈ (V\<rtr>x⇩_{1})\<sad>V" by auto with x(1,3,6) have "k:{⟨s,t⟩∈G×G. t ∈(V\<rtr>s)\<sad>V}" by auto } with V(1) have "{⟨s,t⟩∈G×G. t ∈(W\<rtr>s)\<sad>W} O {⟨s,t⟩∈G×G. t ∈(W\<rtr>s)\<sad>W}⊆U" by auto moreover from W(1) have "{⟨s,t⟩∈G×G. t ∈(W\<rtr>s)\<sad>W}∈roelckeUniformity" unfolding roelckeUniformity_def by auto ultimately show "∃Z∈roelckeUniformity. Z O Z ⊆ U" by auto qed ultimately show "id(G)⊆U ∧ (∃V∈?Φ. V O V ⊆ U) ∧ converse(U) ∈ ?Φ" by simp qed moreover have "roelckeUniformity {is a filter on} (G × G)" proof - { assume "0 ∈ roelckeUniformity" then obtain W where U:"W∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. t ∈(W\<rtr>s)\<sad>W}⊆0" unfolding roelckeUniformity_def by auto have "⟨𝟬,𝟬⟩:G×G" using zero_in_tgroup by auto moreover have "𝟬 = 𝟬\<ra>𝟬\<ra>𝟬" using group0_2_L2 zero_in_tgroup by auto moreover from U(1) have "𝟬∈int(W)" by auto then have "𝟬∈W" using Top_2_L1 by auto with ‹W∈𝒩⇩_{0}› have "𝟬\<ra>𝟬\<ra>𝟬 ∈ (W\<rtr>𝟬)\<sad>W" using group0_2_L2 group_op_closed trans_neutral_image interval_add_zero by auto ultimately have "⟨𝟬,𝟬⟩∈{⟨s,t⟩∈G×G. t ∈(W\<rtr>s)\<sad>W}" by auto with U(2) have False by blast } moreover { fix x xa assume as:"x ∈ roelckeUniformity" "xa∈x" have "roelckeUniformity ⊆ Pow(G×G)" unfolding roelckeUniformity_def by auto with as have "xa ∈ G×G" by auto } moreover { have "G×G∈Pow(G×G)" by auto moreover have "{⟨s,t⟩:G×G. t ∈(G\<rtr>s)\<sad>G} ⊆ G×G" by auto moreover note zneigh_not_empty ultimately have "G×G∈roelckeUniformity" unfolding roelckeUniformity_def by auto } moreover { fix A B assume as:"A∈roelckeUniformity" "B∈roelckeUniformity" from as(1) obtain AU where AU:"AU∈ 𝒩⇩_{0}" "{⟨s,t⟩∈G×G. t ∈(AU\<rtr>s)\<sad>AU}⊆ A" "A∈Pow(G×G)" unfolding roelckeUniformity_def by auto from as(2) obtain BU where BU:"BU∈ 𝒩⇩_{0}" "{⟨s,t⟩∈G×G. t ∈(BU\<rtr>s)\<sad>BU}⊆ B" "B∈Pow(G×G)" unfolding roelckeUniformity_def by auto from AU(1) BU(1) have "𝟬 ∈ int(AU)∩int(BU)" by auto moreover have op:"int(AU)∩int(BU)∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def by auto moreover have "int(AU)∩int(BU) ⊆ AU∩BU" using Top_2_L1 by auto with op have "int(AU)∩int(BU)⊆int(AU∩BU)" using Top_2_L5 by auto moreover note AU(1) BU(1) ultimately have interNeigh:"AU∩BU ∈ 𝒩⇩_{0}" unfolding zerohoods_def by auto moreover { fix z assume "z ∈ {⟨s,t⟩∈G×G. t ∈((AU∩BU)\<rtr>s)\<sad>(AU∩BU)}" then obtain s t where z:"z=⟨s,t⟩" "s∈G" "t∈G" "t ∈ ((AU∩BU)\<rtr>s)\<sad>(AU∩BU)" by force from ‹AU∩BU ∈ 𝒩⇩_{0}› ‹s∈G› have "AU∩BU ⊆ G" and "(AU∩BU)\<rtr>s ⊆G" using lrtrans_in_group_add(2) by auto with z(4) obtain x y where t:"t=x\<ra>y" "x∈(AU∩BU)\<rtr>s" "y∈AU∩BU" using elements_in_set_sum by blast from t(2) z(2) interNeigh obtain q where x:"x=q\<ra>s" "q ∈ AU∩BU" using lrtrans_image(2) by auto with AU(1) BU(1) z(2) have "x ∈ AU\<rtr>s" "x ∈ BU\<rtr>s" using lrtrans_image(2) by auto with ‹y ∈ AU∩BU› ‹AU∈ 𝒩⇩_{0}› ‹BU∈ 𝒩⇩_{0}› ‹s ∈ G› ‹t=x\<ra>y› have "t ∈ (AU\<rtr>s)\<sad>AU" and "t ∈ (BU\<rtr>s)\<sad>BU" using lrtrans_in_group_add(2) elements_in_set_sum_inv by auto with z(1,2,3) have "z ∈ {⟨s,t⟩∈G×G. t ∈(AU\<rtr>s)\<sad>AU}" and "z ∈{⟨s,t⟩∈G×G. t ∈(BU\<rtr>s)\<sad>BU}" by auto } then have "{⟨s,t⟩∈G×G. t ∈((AU∩BU)\<rtr>s)\<sad>(AU∩BU)} ⊆ {⟨s,t⟩∈G×G. t ∈(AU\<rtr>s)\<sad>AU}∩{⟨s,t⟩∈G×G. t ∈(BU\<rtr>s)\<sad>BU}" by auto with AU(2) BU(2) have "{⟨s,t⟩∈G×G. t ∈((AU∩BU)\<rtr>s)\<sad>(AU∩BU)}⊆A∩B" by blast ultimately have "A∩B ∈ roelckeUniformity" using AU(3) BU(3) unfolding roelckeUniformity_def by blast } moreover { fix B C assume as:"B∈roelckeUniformity" "C⊆(G × G)" "B ⊆ C" from as(1) obtain BU where BU:"BU∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. t ∈(BU\<rtr>s)\<sad>BU}⊆B" unfolding roelckeUniformity_def by blast from as(3) BU(2) have "{⟨s,t⟩∈G×G. t ∈(BU\<rtr>s)\<sad>BU}⊆C" by auto then have "C ∈ roelckeUniformity" using as(2) BU(1) unfolding roelckeUniformity_def by auto } ultimately show ?thesis unfolding IsFilter_def by auto qed ultimately show ?thesis using IsUniformity_def by auto qed text‹ The topology given by the roelcke uniformity is the original topology › lemma (in topgroup) top_generated_roelcke_uniformity: shows "UniformTopology(roelckeUniformity,G) = T" proof - let ?M = "{⟨t, {V `` {t} . V ∈ roelckeUniformity}⟩ . t ∈ G}" have fun:"?M:G→Pow(Pow(G))" using IsNeighSystem_def neigh_from_uniformity roelcke_uniformity by auto { fix U assume as:"U ∈ {U ∈ Pow(G). ∀x∈U. U ∈ ?M`x}" { fix x assume x:"x∈U" with as have xg:"x∈G" by auto from x as have "U ∈ {⟨t, {V `` {t} . V ∈ roelckeUniformity}⟩ . t ∈ G}`(x)" by auto with fun ‹x∈G› have "U ∈ {V `` {x} . V ∈ roelckeUniformity}" using ZF_fun_from_tot_val by simp then obtain V where V:"U=V``{x}" "V ∈ roelckeUniformity" by auto from V(2) obtain W where W:"W∈𝒩⇩_{0}" "{⟨s,t⟩∈G×G. t∈ (W\<rtr>s)\<sad>W}⊆V" unfolding roelckeUniformity_def by auto from W(1) have WG:"W⊆G" by auto from W(2) have A:"{⟨s,t⟩:G×G. t:(W\<rtr>s)\<sad>W}``{x} ⊆ V``{x}" by auto have "{⟨s,t⟩ ∈ G×G. t ∈ (W\<rtr>s)\<sad>W}``{x} = (W\<rtr>x)\<sad>W" proof - let ?A = "{⟨s,t⟩:G×G. t ∈ (W\<rtr>s)\<sad>W}" from ‹W⊆G› ‹x∈G› have I:"(W\<rtr>x)\<sad>W ⊆ G" using lrtrans_in_group_add interval_add(1) by auto have "?A``{x} = {t∈G.⟨x,t⟩ ∈ ?A}" by blast moreover have "{t∈G. ⟨x,t⟩ ∈ ?A} ⊆ (W\<rtr>x)\<sad>W" by auto moreover from ‹W⊆G› ‹x∈G› I have "(W\<rtr>x)\<sad>W ⊆ {t∈G. ⟨x,t⟩ ∈ ?A}" by auto ultimately show ?thesis by auto qed with A V(1) have WU:"(W\<rtr>x)\<sad>W ⊆ U" by auto have "int(W)\<rtr>x ⊆ W\<rtr>x" using image_mono Top_2_L1 by simp then have "(int(W)\<rtr>x)×(int(W)) ⊆ (W\<rtr>x)×W" using Top_2_L1 by auto then have "f``((int(W)\<rtr>x)×(int(W))) ⊆ f``((W\<rtr>x)×W)" using image_mono by auto moreover from xg WG have "⟨int(W)\<rtr>x,int(W)⟩ ∈ Pow(G)×Pow(G)" and "⟨(W\<rtr>x),W⟩ ∈ Pow(G)×Pow(G)" using Top_2_L2 lrtrans_in_group_add(2) by auto then have "(int(W)\<rtr>x)\<sad>(int(W)) = f``((int(W)\<rtr>x)×(int(W)))" and "(W\<rtr>x)\<sad>W = f``((W\<rtr>x)×W)" using interval_add(2) by auto ultimately have "(int(W)\<rtr>x)\<sad>(int(W)) ⊆ (W\<rtr>x)\<sad>W" by auto with xg WG have "int(W\<rtr>x)\<sad>(int(W)) ⊆ (W\<rtr>x)\<sad>W" using rtrans_interior by auto moreover { have "int(W\<rtr>x)\<sad>(int(W)) = (⋃t∈int(W\<rtr>x). t\<ltr>(int(W)))" using interval_add(3) Top_2_L2 by auto moreover have "∀t∈int(W\<rtr>x). t\<ltr>(int(W)) = int(t\<ltr>W)" proof - { fix t assume "t ∈ int(W\<rtr>x)" from ‹x∈G› have "(W\<rtr>x) ⊆ G" using lrtrans_in_group_add(2) by simp with ‹t ∈ int(W\<rtr>x)› have "t∈G" using Top_2_L2 by auto with ‹W⊆G› have "t \<ltr> int(W) = int(t\<ltr>W)" using ltrans_interior by simp } thus ?thesis by simp qed ultimately have "int(W\<rtr>x)\<sad>(int(W)) = (⋃t∈int(W\<rtr>x). int(t\<ltr>W))" by auto with topSpaceAssum have "int(W\<rtr>x)\<sad>(int(W)) ∈ T" using Top_2_L2 union_open by auto } moreover from ‹x∈G› ‹W∈𝒩⇩_{0}› have "x ∈ int(W\<rtr>x)\<sad>(int(W))" using elem_in_int_rtrans(2) by simp moreover note WU ultimately have "∃Y∈T. x∈Y ∧ Y⊆U" by auto } then have "U∈T" using open_neigh_open by auto } then have "{U ∈ Pow(G). ∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ roelckeUniformity}⟩ . t ∈ G}`(x)} ⊆ T" by auto moreover { fix U assume op:"U∈T" { fix x assume x:"x∈U" with op have xg:"x∈G" by auto have "(\<rm>x)\<ltr>U ∈ 𝒩⇩_{0}" using open_trans_neigh op x by auto then obtain W where W:"W∈𝒩⇩_{0}" "W \<sad> W ⊆(\<rm>x)\<ltr>U" using exists_procls_zerohood by blast let ?V = "x\<ltr>(W\<rtr>(\<rm>x)) ∩ W" from ‹W ∈ 𝒩⇩_{0}› ‹x∈G› have xWx:"x\<ltr>(W\<rtr>(\<rm>x)) :𝒩⇩_{0}" using lrtrans_neigh by simp from W(1) have WG:"W⊆G" by auto from xWx W(1) have "𝟬∈int(x\<ltr>(W\<rtr>(\<rm>x)))∩int(W)" by auto have int:"int(x\<ltr>(W\<rtr>(\<rm>x)))∩int(W)∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def by auto have "int(x\<ltr>(W\<rtr>(\<rm>x)))∩int(W) ⊆ (x\<ltr>(W\<rtr>(\<rm>x)))∩W" using Top_2_L1 by auto with int have "int(x\<ltr>(W\<rtr>(\<rm>x)))∩int(W)⊆int((x\<ltr>(W\<rtr>(\<rm>x)))∩W)" using Top_2_L5 by auto moreover note xWx W(1) ultimately have V_NEIG:"?V ∈ 𝒩⇩_{0}" unfolding zerohoods_def by auto { fix z assume z:"z ∈ (?V\<rtr>x)\<sad>?V" from W(1) have VG:"?V ⊆ G" by auto with ‹x∈G› have VxG:"?V\<rtr>x ⊆ G" using lrtrans_in_group_add(2) by simp from z VG VxG W(1) obtain a⇩_{1}b⇩_{1}where ab:"z=a⇩_{1}\<ra>b⇩_{1}" "a⇩_{1}∈ ?V\<rtr>x" "b⇩_{1}∈ ?V" using elements_in_set_sum by blast from ab(2) xg VG obtain c⇩_{1}where c:"a⇩_{1}=c⇩_{1}\<ra>x" "c⇩_{1}∈ ?V" using elements_in_rtrans by blast from ab(3) c(2) have bc:"b⇩_{1}∈W" "c⇩_{1}∈ x\<ltr>(W\<rtr>(\<rm>x))" by auto from ‹x∈G› have "x\<ltr>(W\<rtr>(\<rm>x)) = {x\<ra>y. y∈(W\<rtr>(\<rm>x))}" using neg_in_tgroup lrtrans_in_group_add lrtrans_image by auto with ‹c⇩_{1}∈ x\<ltr>(W\<rtr>(\<rm>x))› obtain d where d:"c⇩_{1}=x\<ra>d" "d ∈ W\<rtr>(\<rm>x)" by auto from ‹x∈G› ‹W∈𝒩⇩_{0}› ‹d ∈ W\<rtr>(\<rm>x)› obtain e where e:"d=e\<ra>(\<rm>x)" "e∈W" using neg_in_tgroup lrtrans_in_group lrtrans_image(2) by auto from e(2) WG have eG:"e∈G" by auto from ‹e∈W› ‹W⊆G› ‹b⇩_{1}∈W› have "e∈G" "b⇩_{1}∈G" by auto from ‹z = a⇩_{1}\<ra>b⇩_{1}› ‹a⇩_{1}= c⇩_{1}\<ra>x› ‹c⇩_{1}= x\<ra>d› ‹d = e\<ra>(\<rm>x)› have "z = x \<ra> (e\<ra>(\<rm>x)) \<ra> x \<ra> b⇩_{1}" by simp with ‹x∈G› ‹e∈G› have "z=(x\<ra>e)\<ra>b⇩_{1}" using cancel_middle(4) by simp with ‹x∈G› ‹e∈G› ‹b⇩_{1}∈G› have "z = x\<ra>(e\<ra>b⇩_{1})" using group_oper_assoc by simp moreover from e(2) ab(3) WG have "e\<ra>b⇩_{1}∈ W\<sad>W" using elements_in_set_sum_inv by auto moreover note xg WG ultimately have "z∈x\<ltr>(W\<sad>W)" using elements_in_ltrans_inv interval_add(1) by auto moreover from ‹W⊆G› ‹U∈T› have "W \<sad> W ⊆ G" and "U⊆G" using interval_add(1) by auto with ‹W \<sad> W ⊆(\<rm>x)\<ltr>U› ‹x∈G› have "x\<ltr>(W\<sad>W) ⊆ U" using trans_subset by simp ultimately have "z∈U" by auto } then have sub:"(?V\<rtr>x)\<sad>?V ⊆ U" by auto moreover from V_NEIG have unif:"{⟨s,t⟩ ∈ G×G. t : (?V\<rtr>s)\<sad>?V} ∈ roelckeUniformity" unfolding roelckeUniformity_def by auto moreover from xg have "∀q. q∈{⟨s,t⟩ ∈ G×G. t : (?V\<rtr>s)\<sad>?V}``{x} ⟷ q∈((?V\<rtr>x)\<sad>?V)∩G" by auto then have "{⟨s,t⟩ ∈ G×G. t ∈ (?V\<rtr>s)\<sad>?V}``{x} = ((?V\<rtr>x)\<sad>?V)∩G" by auto ultimately have basic:"{⟨s,t⟩ ∈ G×G. t : (?V\<rtr>s)\<sad>?V}``{x} ⊆ U" using op by auto have add:"({x}×U)``{x} =U" by auto from basic add have "({⟨s,t⟩ ∈ G×G. t ∈ (?V\<rtr>s)\<sad>?V}∪({x}×U))``{x} = U" by auto moreover have R:"∀B∈roelckeUniformity.(∀ C∈Pow(G × G). B ⊆ C ⟶ C ∈ roelckeUniformity)" using roelcke_uniformity unfolding IsUniformity_def IsFilter_def by auto moreover from op xg have GG:"({⟨s,t⟩ ∈ G×G. t ∈ (?V\<rtr>s)\<sad>?V}∪({x}×U)):Pow(G×G)" by auto moreover have "{⟨s,t⟩ ∈ G×G. t∈(?V\<rtr>s)\<sad>?V} ⊆ ({⟨s,t⟩ ∈ G×G. t∈(?V\<rtr>s)\<sad>?V}∪({x}×U))" by auto moreover from R unif GG have "({⟨s,t⟩ ∈ G×G. t ∈ (?V\<rtr>s)\<sad>?V}∪({x}×U)) ∈ roelckeUniformity" by auto ultimately have "∃V∈roelckeUniformity. V``{x} = U" by auto then have "U ∈ {V `` {x} . V ∈ roelckeUniformity}" by auto with xg fun have "U ∈ {⟨t, {V `` {t} . V ∈ roelckeUniformity}⟩ . t ∈ G} ` x" using apply_equality by auto } hence "∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ roelckeUniformity}⟩ . t ∈ G} ` x" by auto with op have "U:{U ∈ Pow(G). ∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ roelckeUniformity}⟩ . t ∈ G}`(x)}" by auto } then have "T ⊆ {U ∈ Pow(G). ∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ roelckeUniformity}⟩ . t ∈ G}`(x)}" by auto ultimately have "{U ∈ Pow(G). ∀x∈U. U ∈ {⟨t, {V `` {t} . V ∈ roelckeUniformity}⟩ . t ∈ G}`(x)} = T" by auto then show ?thesis using uniftop_def_alt by simp qed text‹The inverse map is uniformly continuous in the Roelcke uniformity› theorem (in topgroup) inv_uniform_roelcke: shows "GroupInv(G,f) {is uniformly continuous between} roelckeUniformity {and} roelckeUniformity" proof - let ?P = "ProdFunction(GroupInv(G,f), GroupInv(G,f))" have L: "GroupInv(G,f):G→G" and R:"roelckeUniformity {is a uniformity on} G" using groupAssum group0_2_T2 roelcke_uniformity by auto have "∀V ∈ roelckeUniformity. ?P-``(V) ∈ roelckeUniformity" proof fix V assume v:"V∈ roelckeUniformity" then obtain U where "U ∈ 𝒩⇩_{0}" and "{⟨s,t⟩ ∈ G × G . t ∈ U \<rtr> s \<sad> U} ⊆ V" unfolding roelckeUniformity_def by auto with ‹V ∈ roelckeUniformity› have as:"V ⊆ G × G" "U ∈ 𝒩⇩_{0}" "{⟨s,t⟩ ∈ G × G . t ∈ U \<rtr> s \<sad> U} ⊆ V" unfolding roelckeUniformity_def by auto from as(2) obtain W where w:"W ∈ 𝒩⇩_{0}" "W ⊆ U" "(\<sm>W) = W" using exists_sym_zerohood by blast from w(1) have wg:"W⊆G" by auto { fix z assume z:"z ∈ {⟨s,t⟩ ∈ G × G . t ∈ W \<rtr> s \<sad> W}" then obtain s t where st:"z=⟨s,t⟩" "s∈G" "t∈G" by auto from st(1) z have st2: "t ∈ W \<rtr> s \<sad> W" by auto with ‹W ∈ 𝒩⇩_{0}› st(2) obtain u v where uv:"t=u\<ra>v" "u∈W\<rtr>s" "v∈W" using interval_add(4) lrtrans_in_group_add(2) by auto from ‹W⊆G› ‹s∈G› ‹u∈W\<rtr>s› obtain q where q:"q∈W" "u=q\<ra>s" using elements_in_rtrans by blast from w(2) as(2) q st(2) have "u∈U\<rtr>s" using lrtrans_image(2) by auto with w(2) uv(1,3) as(2) st(2) have "t∈U \<rtr> s \<sad> U" using interval_add(4) lrtrans_in_group_add(2) by auto with st have "z ∈ {⟨s,t⟩ ∈ G × G . t ∈ U \<rtr> s \<sad> U}" by auto } then have sub:"{⟨s,t⟩ ∈ G × G . t ∈ W \<rtr> s \<sad> W} ⊆ {⟨s,t⟩ ∈ G × G . t ∈ U \<rtr> s \<sad> U}" by auto { fix z assume z:"z ∈ {⟨s,t⟩ ∈ G × G . t ∈ W \<rtr> s \<sad> W}" then obtain s t where st:"z=⟨s,t⟩" "s∈G" "t∈G" by auto from st(1) z have st2: "t ∈ W \<rtr> s \<sad> W" by auto with ‹W ∈ 𝒩⇩_{0}› obtain u v where uv:"t=u\<ra>v" "u∈W\<rtr>s" "v∈W" using interval_add(4) lrtrans_in_group_add(2) st(2) by auto from ‹W⊆G› ‹s∈G› ‹u∈W\<rtr>s› obtain q where q:"q∈W" "u=q\<ra>s" using elements_in_rtrans by blast from ‹W⊆G› ‹q∈W› ‹v∈W› have "q∈G" "v∈G" by auto with ‹q∈G› ‹v∈G› ‹u=q\<ra>s› st(2) uv(1) q(2) have "t=q\<ra>(s\<ra>v)" using group_op_closed_add group_oper_assoc by auto with st(2) ‹q∈G› ‹v∈G› have minust:"(\<rm>t) = (\<rm>v)\<ra>(\<rm>s)\<ra>(\<rm>q)" using group_inv_of_two group_op_closed group_inv_of_two by auto from q(1) wg have "(\<rm>q)∈\<sm>W" using ginv_image_add(2) by auto with w(3) have minusq:"(\<rm>q)∈W" by auto from uv(3) wg have "(\<rm>v)∈\<sm>W" using ginv_image_add(2) by auto with w(3) have minusv:"(\<rm>v)∈W" by auto with st(2) wg have "(\<rm>v)\<ra>(\<rm>s) ∈ W\<rtr>(\<rm>s)" using lrtrans_image(2) inverse_in_group by auto with minust minusq st(2) wg have "(\<rm>t)∈(W\<rtr>(\<rm>s))\<sad>W" using interval_add(4) inverse_in_group lrtrans_in_group_add(2) by auto moreover from st groupAssum have "?P`(z) = ⟨GroupInv(G,f)`(s), GroupInv(G,f)`(t)⟩" using prodFunctionApp group0_2_T2 by blast with st(2,3) have "?P`(z) = ⟨\<rm>s,\<rm>