Theory TopologicalGroup_Uniformity_ZF
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>t⟩" by auto
ultimately have "?P`(z) ∈ {⟨s,t⟩ ∈ G × G . t ∈ W \<rtr> s \<sad> W}"
using st(2,3) inverse_in_group by auto
with sub have "?P`(z) ∈ {⟨s,t⟩ ∈ G × G . t ∈ U \<rtr> s \<sad> U}" by force
with as(3) have "?P`(z) ∈ V" by force
with z L have "z ∈ ?P-``(V)" using prodFunction func1_1_L5A vimage_iff
by blast
}
with w(1) have "∃U∈𝒩⇩0. {⟨s,t⟩ ∈ G × G . t ∈ U \<rtr> s \<sad> U} ⊆ ?P-``(V)"
by blast
with L show "?P-``(V) ∈ roelckeUniformity"
unfolding roelckeUniformity_def using prodFunction func1_1_L6A by blast
qed
with L R show ?thesis using IsUniformlyCont_def by auto
qed
end