IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory TopologicalGroup_Uniformity_ZF imports TopologicalGroup_ZF UniformSpace_ZF_1
begin

Each topological group is a uniform space. This theory is about the unifomities that are naturally defined by a topological group structure.

Topological group: definition and notation

There are two basic uniformities that can be defined on a topological group.

Definition of left uniformity

Definition (in topgroup)

\( \text{ leftUniformity } \equiv \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in U\} \subseteq V\} \)

Definition of right uniformity

Definition (in topgroup)

\( \text{ rightUniformity } \equiv \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in U\}\subseteq V\} \)

Right and left uniformities are indeed uniformities.

lemma (in topgroup) side_uniformities:

shows \( \text{ leftUniformity } \text{ is a uniformity on } G \) and \( \text{ rightUniformity } \text{ is a uniformity on } G \)proof
{
assume \( 0 \in \text{ leftUniformity } \)
then obtain \( U \) where U: \( U\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in U\}\subseteq 0 \) unfolding leftUniformity_def
have \( \langle 0 , 0 \rangle :G\times G \) using zero_in_tgroup
moreover
have \( ( - 0 ) + 0 = 0 \) using group0_valid_in_tgroup , group_inv_of_one , group0_2_L2 , zero_in_tgroup
moreover
have \( 0 \in int(U) \) using U(1)
then have \( 0 \in U \) using Top_2_L1
ultimately have \( \langle 0 , 0 \rangle \in \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in U\} \)
with U(2) have \( \langle 0 , 0 \rangle \in 0 \)
hence \( False \)
}
hence \( 0\notin \text{ leftUniformity } \)
moreover
have \( \text{ leftUniformity } \subseteq Pow(G\times G) \) unfolding leftUniformity_def
moreover {
have \( G\times G\in Pow(G\times G) \)
moreover
have \( \{\langle s,t\rangle :G\times G.\ ( - s) + t:G\} \subseteq G\times G \)
moreover
note zneigh_not_empty
ultimately have \( G\times G\in \text{ leftUniformity } \) unfolding leftUniformity_def
} moreover {
fix \( A \) \( B \)
assume as: \( A\in \text{ leftUniformity } \), \( B\in \text{ leftUniformity } \)
from as(1) obtain \( AU \) where AU: \( AU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in AU\}\subseteq A \), \( A\in Pow(G\times G) \) unfolding leftUniformity_def
from as(2) obtain \( BU \) where BU: \( BU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in BU\}\subseteq B \), \( B\in Pow(G\times G) \) unfolding leftUniformity_def
from AU(1), BU(1) have \( 0 \in int(AU)\cap int(BU) \)
moreover
from AU, BU have op: \( int(AU)\cap int(BU)\in T \) using Top_2_L2 , topSpaceAssum , IsATopology_def
moreover
have \( int(AU)\cap int(BU) \subseteq AU\cap BU \) using Top_2_L1
with op have \( int(AU)\cap int(BU)\subseteq int(AU\cap BU) \) using Top_2_L5
moreover
note AU(1), BU(1)
ultimately have \( AU\cap BU: \mathcal{N}_0 \) unfolding zerohoods_def
moreover
have \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in AU\cap BU\}\subseteq \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in AU\} \)
with AU(2), BU(2) have \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in AU\cap BU\}\subseteq A\cap B \)
ultimately have \( A\cap B \in \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in U\} \subseteq V\} \) using AU(3) , BU(3)
then have \( A\cap B\in \text{ leftUniformity } \) unfolding leftUniformity_def
}
hence \( \forall A\in \text{ leftUniformity }.\ \forall B\in \text{ leftUniformity }.\ A \cap B \in \text{ leftUniformity } \)
moreover {
fix \( B \) \( C \)
assume as: \( B\in \text{ leftUniformity } \), \( C\in Pow(G \times G) \), \( B \subseteq C \)
from as(1) obtain \( BU \) where BU: \( BU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in BU\}\subseteq B \) unfolding leftUniformity_def
from as(3), BU(2) have \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in BU\}\subseteq C \)
with as(2), BU(1) have \( C \in \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in U\} \subseteq V\} \)
then have \( C \in \text{ leftUniformity } \) unfolding leftUniformity_def
}
then have \( \forall B\in \text{ leftUniformity }.\ \forall C\in Pow(G\times G).\ B\subseteq C \longrightarrow C\in \text{ leftUniformity } \)
ultimately have leftFilter: \( \text{ leftUniformity } \text{ is a filter on } (G\times G) \) unfolding IsFilter_def
{
assume \( 0\in \text{ rightUniformity } \)
then obtain \( U \) where U: \( U\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in U\}\subseteq 0 \) unfolding rightUniformity_def
have \( \langle 0 , 0 \rangle :G\times G \) using zero_in_tgroup
moreover
have \( 0 + ( - 0 ) = 0 \) using group0_valid_in_tgroup , group_inv_of_one , group0_2_L2 , zero_in_tgroup
moreover
have \( 0 \in int(U) \) using U(1)
then have \( 0 \in U \) using Top_2_L1
ultimately have \( \langle 0 , 0 \rangle \in \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in U\} \)
with U(2) have \( \langle 0 , 0 \rangle \in 0 \)
hence \( False \)
}
then have \( 0\notin \text{ rightUniformity } \)
moreover
have \( \text{ rightUniformity } \subseteq Pow(G\times G) \) unfolding rightUniformity_def
moreover {
have \( G\times G\in Pow(G\times G) \)
moreover
have \( \{\langle s,t\rangle :G\times G.\ ( - s) + t:G\} \subseteq G\times G \)
moreover
note zneigh_not_empty
ultimately have \( G\times G \in \text{ rightUniformity } \) unfolding rightUniformity_def
} moreover {
fix \( A \) \( B \)
assume as: \( A\in \text{ rightUniformity } \), \( B\in \text{ rightUniformity } \)
from as(1) obtain \( AU \) where AU: \( AU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in AU\}\subseteq A \), \( A\in Pow(G\times G) \) unfolding rightUniformity_def
from as(2) obtain \( BU \) where BU: \( BU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in BU\}\subseteq B \), \( B\in Pow(G\times G) \) unfolding rightUniformity_def
from AU(1), BU(1) have \( 0 \in int(AU)\cap int(BU) \)
moreover
from AU, BU have op: \( int(AU)\cap int(BU)\in T \) using Top_2_L2 , topSpaceAssum , IsATopology_def
moreover
have \( int(AU)\cap int(BU) \subseteq AU\cap BU \) using Top_2_L1
with op have \( int(AU)\cap int(BU)\subseteq int(AU\cap BU) \) using Top_2_L5
moreover
note AU(1), BU(1)
ultimately have \( AU\cap BU: \mathcal{N}_0 \) unfolding zerohoods_def
moreover
have \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in AU\cap BU\}\subseteq \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in AU\} \)
with AU(2), BU(2) have \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in AU\cap BU\}\subseteq A\cap B \)
ultimately have \( A\cap B \in \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in U\}\subseteq V\} \) using AU(3) , BU(3)
then have \( A\cap B \in \text{ rightUniformity } \) unfolding rightUniformity_def
}
hence \( \forall A\in \text{ rightUniformity }.\ \forall B\in \text{ rightUniformity }.\ A\cap B \in \text{ rightUniformity } \)
moreover {
fix \( B \) \( C \)
assume as: \( B\in \text{ rightUniformity } \), \( C\in Pow(G \times G) \), \( B \subseteq C \)
from as(1) obtain \( BU \) where BU: \( BU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in BU\}\subseteq B \) unfolding rightUniformity_def
from as(3), BU(2) have \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in BU\}\subseteq C \)
then have \( C \in \text{ rightUniformity } \) using as(2) , BU(1) unfolding rightUniformity_def
}
then have \( \forall B\in \text{ rightUniformity }.\ \forall C\in Pow(G\times G).\ B\subseteq C \longrightarrow C\in \text{ rightUniformity } \)
ultimately have rightFilter: \( \text{ rightUniformity } \text{ is a filter on } (G\times G) \) unfolding IsFilter_def
{
fix \( U \)
assume as: \( U\in \text{ leftUniformity } \)
from as obtain \( V \) where V: \( V\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in V\} \subseteq U \) unfolding leftUniformity_def
then have \( V\subseteq G \)
{
fix \( x \)
assume as2: \( x\in id(G) \)
from as obtain \( V \) where V: \( V\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in V\} \subseteq U \) unfolding leftUniformity_def
from V(1) have \( 0 \in int(V) \)
then have V0: \( 0 \in V \) using Top_2_L1
from as2 obtain \( t \) where t: \( x=\langle t,t\rangle \), \( t:G \)
from t(2) have \( ( - t) + t = 0 \) using group0_valid_in_tgroup , group0_2_L6
with V0, t, V(2) have \( x\in U \)
}
then have \( id(G)\subseteq U \)
moreover {
{
fix \( x \)
assume ass: \( x\in \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in -V\} \)
then obtain \( s \) \( t \) where as: \( s\in G \), \( t\in G \), \( ( - s) + t \in -V \), \( x=\langle s,t\rangle \)
from as(3), \( V\subseteq G \) have \( ( - s) + t\in \{ - q.\ q\in V\} \) using ginv_image_add
then obtain \( q \) where q: \( q\in V \), \( ( - s) + t = - q \)
with \( V\subseteq G \) have \( q\in G \)
with \( s\in G \), \( t\in G \), \( ( - s) + t = - q \) have \( q=( - t) + s \) using simple_equation1_add
with q(1) have \( ( - t) + s \in V \)
with as(1,2) have \( \langle t,s\rangle \in U \) using V(2)
then have \( \langle s,t\rangle \in converse(U) \)
with as(4) have \( x \in converse(U) \)
}
then have \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in -V\} \subseteq converse(U) \)
moreover
have \( (-V):\mathcal{N}_0 \) using neg_neigh_neigh , V(1)
moreover
note as
ultimately have \( converse(U) \in \text{ leftUniformity } \) unfolding leftUniformity_def
} moreover {
from V(1) obtain \( W \) where W: \( W:\mathcal{N}_0 \), \( W + W \subseteq V \) using exists_procls_zerohood
{
fix \( x \)
assume as: \( x \in \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in W\}\circ \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in W\} \)
then obtain \( x_1 \) \( x_2 \) \( x_3 \) where x: \( x_1\in G \), \( x_2\in G \), \( x_3\in G \), \( ( - x_1) + x_2 \in W \), \( ( - x_2) + x_3 \in W \), \( x=\langle x_1,x_3\rangle \) unfolding comp_def
from W(1) have \( W + W = f(W\times W) \) using interval_add(2)
moreover
from W(1) have WW: \( W\times W\subseteq G\times G \)
moreover
from x(4,5) have \( \langle ( - x_1) + x_2,( - x_2) + x_3\rangle :W\times W \)
with WW have \( f(\langle ( - x_1) + x_2,( - x_2) + x_3\rangle ):f(W\times W) \) using func_imagedef , topgroup_f_binop
ultimately have \( (( - x_1) + x_2) + (( - x_2) + x_3) :W + W \)
moreover
from x(1,2,3) have \( (( - x_1) + x_2) + (( - x_2) + x_3) = ( - x_1) + x_3 \) using cancel_middle_add(2)
ultimately have \( ( - x_1) + x_3\in W + W \)
with W(2) have \( ( - x_1) + x_3\in V \)
with x(1,3,6) have \( x:\{\langle s,t\rangle \in G\times G.\ ( - s) + t \in V\} \)
}
then have \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in W\}\circ \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in W\} \subseteq U \) using V(2)
moreover
have \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in W\}\in \text{ leftUniformity } \) unfolding leftUniformity_def using W(1)
ultimately have \( \exists Z\in \text{ leftUniformity }.\ Z\circ Z\subseteq U \)
} ultimately have \( id(G)\subseteq U \wedge (\exists Z\in \text{ leftUniformity }.\ Z\circ Z\subseteq U) \wedge converse(U)\in \text{ leftUniformity } \)
}
then have \( \forall U\in \text{ leftUniformity }.\ id(G)\subseteq U \wedge (\exists Z\in \text{ leftUniformity }.\ Z\circ Z\subseteq U) \wedge converse(U)\in \text{ leftUniformity } \)
with leftFilter show \( \text{ leftUniformity } \text{ is a uniformity on } G \) unfolding IsUniformity_def
{
fix \( U \)
assume as: \( U\in \text{ rightUniformity } \)
from as obtain \( V \) where V: \( V\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in V\} \subseteq U \) unfolding rightUniformity_def
{
fix \( x \)
assume as2: \( x\in id(G) \)
from as obtain \( V \) where V: \( V\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in V\} \subseteq U \) unfolding rightUniformity_def
from V(1) have \( 0 \in int(V) \)
then have V0: \( 0 \in V \) using Top_2_L1
from as2 obtain \( t \) where t: \( x=\langle t,t\rangle \), \( t:G \)
from t(2) have \( t + ( - t) = 0 \) using group0_valid_in_tgroup , group0_2_L6
with V0, t, V(2) have \( x\in U \)
}
then have \( id(G)\subseteq U \)
moreover {
{
fix \( x \)
assume ass: \( x\in \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in -V\} \)
then obtain \( s \) \( t \) where as: \( s\in G \), \( t\in G \), \( s + ( - t) \in -V \), \( x=\langle s,t\rangle \)
from as(3), V(1) have \( s + ( - t) \in \{ - q.\ q\in V\} \) using ginv_image_add
then obtain \( q \) where q: \( q\in V \), \( s + ( - t) = - q \)
with \( V\in \mathcal{N}_0 \) have \( q\in G \)
with as(1,2), q(1,2) have \( t + ( - s) \in V \) using simple_equation0_add
with as(1,2,4), V(2) have \( x \in converse(U) \)
}
then have \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in -V\} \subseteq converse(U) \)
moreover
from V(1) have \( (-V) \in \mathcal{N}_0 \) using neg_neigh_neigh
ultimately have \( converse(U) \in \text{ rightUniformity } \) using as , rightUniformity_def
} moreover {
from V(1) obtain \( W \) where W: \( W:\mathcal{N}_0 \), \( W + W \subseteq V \) using exists_procls_zerohood
{
fix \( x \)
assume as: \( x:\{\langle s,t\rangle \in G\times G.\ s + ( - t) \in W\}\circ \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in W\} \)
then obtain \( x_1 \) \( x_2 \) \( x_3 \) where x: \( x_1:G \), \( x_2\in G \), \( x_3\in G \), \( x_1 + ( - x_2) \in W \), \( x_2 + ( - x_3) \in W \), \( x=\langle x_1,x_3\rangle \) unfolding comp_def
from W(1) have \( W + W = f(W\times W) \) using interval_add(2)
moreover
from W(1) have WW: \( W\times W\subseteq G\times G \)
moreover
from x(4,5) have \( \langle x_1 + ( - x_2),x_2 + ( - x_3)\rangle \in W\times W \)
with WW have \( f(\langle x_1 + ( - x_2),x_2 + ( - x_3)\rangle ) \in f(W\times W) \) using func_imagedef , topgroup_f_binop
ultimately have \( (x_1 + ( - x_2)) + (x_2 + ( - x_3)) \in W + W \)
moreover
from x(1,2,3) have \( (x_1 + ( - x_2)) + (x_2 + ( - x_3)) = x_1 + ( - x_3) \) using cancel_middle_add(1)
ultimately have \( x_1 + ( - x_3) \in W + W \)
with W(2) have \( x_1 + ( - x_3) \in V \)
then have \( x \in \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in V\} \) using x(1,3,6)
}
with V(2) have \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in W\}\circ \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in W\} \subseteq U \)
moreover
from W(1) have \( \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in W\} \in \text{ rightUniformity } \) unfolding rightUniformity_def
ultimately have \( \exists Z\in \text{ rightUniformity }.\ Z\circ Z\subseteq U \)
} ultimately have \( id(G)\subseteq U \wedge (\exists Z\in \text{ rightUniformity }.\ Z\circ Z\subseteq U) \wedge converse(U)\in \text{ rightUniformity } \)
}
then have \( \forall U\in \text{ rightUniformity }.\ id(G)\subseteq U \wedge (\exists Z\in \text{ rightUniformity }.\ Z\circ Z\subseteq U) \wedge converse(U)\in \text{ rightUniformity } \)
with rightFilter show \( \text{ rightUniformity } \text{ is a uniformity on } G \) unfolding IsUniformity_def
qed

The topologies generated by the right and left uniformities are the original group topology.

lemma (in topgroup) top_generated_side_uniformities:

shows \( \text{UniformTopology}(\text{ leftUniformity },G) = T \) and \( \text{UniformTopology}(\text{ rightUniformity },G) = T \)proof
let \( M = \{\langle t, \{V \{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t\in G\} \)
have fun: \( M:G\rightarrow Pow(Pow(G)) \) using neigh_from_uniformity , side_uniformities(1) , IsNeighSystem_def
let \( N = \{\langle t, \{V \{t\} .\ V \in \text{ rightUniformity }\}\rangle .\ t\in G\} \)
have funN: \( N:G\rightarrow Pow(Pow(G)) \) using neigh_from_uniformity , side_uniformities(2) , IsNeighSystem_def
{
fix \( U \)
assume op: \( U\in T \)
hence \( U\subseteq G \)
{
fix \( x \)
assume x: \( x\in U \)
with op have xg: \( x\in G \) and \( ( - x) \in G \) using neg_in_tgroup
then have \( \langle x, \{V\{x\}.\ V \in \text{ leftUniformity }\}\rangle \in \{\langle t, \{V\{t\}.\ V \in \text{ leftUniformity }\}\rangle .\ t\in G\} \)
with fun have app: \( M(x) = \{V\{x\}.\ V \in \text{ leftUniformity }\} \) using ZF_fun_from_tot_val
have \( ( - x) + U : \mathcal{N}_0 \) using open_trans_neigh , op , x
then have V: \( \{\langle s,t\rangle \in G\times G.\ ( - s) + t\in (( - x) + U)\} \in \text{ leftUniformity } \) unfolding leftUniformity_def
with xg have N: \( \forall t\in G.\ t:\{\langle s,t\rangle \in G\times G.\ ( - s) + t\in (( - x) + U)\}\{x\} \longleftrightarrow ( - x) + t\in (( - x) + U) \) using image_iff
{
fix \( t \)
assume t: \( t\in G \)
{
assume as: \( ( - x) + t\in (( - x) + U) \)
then have \( ( - x) + t\in \text{LeftTranslation}(G,f, - x)U \)
then obtain \( q \) where q: \( q\in U \), \( \langle q,( - x) + t\rangle \in \text{LeftTranslation}(G,f, - x) \) using image_iff
with op have \( q\in G \)
from q(2) have \( ( - x) + q = ( - x) + t \) unfolding LeftTranslation_def
with \( ( - x) \in G \), \( q\in G \), \( t\in G \) have \( q = t \) using neg_in_tgroup , cancel_left_add
with q(1) have \( t\in U \)
}
moreover {
assume t: \( t\in U \)
with \( U\subseteq G \), \( ( - x)\in G \) have \( ( - x) + t \in (( - x) + U) \) using lrtrans_image(1)
} ultimately have \( ( - x) + t\in (( - x) + U) \longleftrightarrow t:U \)
}
with N have \( \forall t\in G.\ t:\{\langle s,t\rangle \in G\times G.\ ( - s) + t \in (( - x) + U)\}\{x\} \longleftrightarrow t\in U \)
with op have \( \forall t.\ t:\{\langle s,t\rangle \in G\times G.\ ( - s) + t\in (( - x) + U)\}\{x\} \longleftrightarrow t:U \)
hence \( U = \{\langle s,t\rangle \in G\times G.\ ( - s) + t\in (( - x) + U)\}\{x\} \)
with V have \( \exists V\in \text{ leftUniformity }.\ U=V\{x\} \)
with app have \( U \in \{\langle t, \{V \{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t \in G\}(x) \)
moreover
from \( x\in G \), funN have app: \( N(x) = \{V\{x\}.\ V \in \text{ rightUniformity }\} \) using ZF_fun_from_tot_val
moreover
from x, op have openTrans: \( U + ( - x): \mathcal{N}_0 \) using open_trans_neigh_2
then have V: \( \{\langle s,t\rangle \in G\times G.\ s + ( - t)\in (U + ( - x))\} \in \text{ rightUniformity } \) unfolding rightUniformity_def
with xg have N: \( \forall t\in G.\ t:\{\langle s,t\rangle \in G\times G.\ s + ( - t)\in (U + ( - x))\}^{-1}\{x\} \longleftrightarrow t + ( - x)\in (U + ( - x)) \) using vimage_iff
moreover {
fix \( t \)
assume t: \( t\in G \)
{
assume as: \( t + ( - x)\in (U + ( - x)) \)
hence \( t + ( - x)\in \text{RightTranslation}(G,f, - x)U \)
then obtain \( q \) where q: \( q\in U \), \( \langle q,t + ( - x)\rangle \in \text{RightTranslation}(G,f, - x) \) using image_iff
with op have \( q\in G \)
from q(2) have \( q + ( - x) = t + ( - x) \) unfolding RightTranslation_def
with \( q\in G \), \( ( - x) \in G \), \( t\in G \) have \( q = t \) using cancel_right_add
with q(1) have \( t\in U \)
}
moreover {
assume \( t\in U \)
with \( ( - x)\in G \), \( U\subseteq G \) have \( t + ( - x)\in (U + ( - x)) \) using lrtrans_image(2)
} ultimately have \( t + ( - x)\in (U + ( - x)) \longleftrightarrow t:U \)
}
with N have \( \forall t\in G.\ t:\{\langle s,t\rangle \in G\times G.\ s + ( - t)\in (U + ( - x))\}^{-1}\{x\} \longleftrightarrow t:U \)
with op have \( \forall t.\ t:\{\langle s,t\rangle \in G\times G.\ s + ( - t)\in (U + ( - x))\}^{-1}\{x\} \longleftrightarrow t:U \)
hence \( \{\langle s,t\rangle \in G\times G.\ s + ( - t)\in (U + ( - x))\}^{-1}\{x\} = U \)
then have \( U = converse(\{\langle s,t\rangle \in G\times G.\ s + ( - t)\in (U + ( - x))\})\{x\} \) unfolding vimage_def
with V, app have \( U \in \{\langle t, \{V \{t\} .\ V \in \text{ rightUniformity }\}\rangle .\ t \in G\}(x) \) using side_uniformities(2) , IsUniformity_def
ultimately have \( U \in \{\langle t, \{V \{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t \in G\}(x) \) and \( U \in \{\langle t, \{V \{t\} .\ V \in \text{ rightUniformity }\}\rangle .\ t \in G\}(x) \)
}
hence \( \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t \in G\} x \) and \( \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{ rightUniformity }\}\rangle .\ t \in G\} x \)
}
hence \( T\subseteq \{U \in Pow(G) .\ \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t \in G\} x\} \) and \( T\subseteq \{U \in Pow(G) .\ \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{ rightUniformity }\}\rangle .\ t \in G\} x\} \)
moreover {
fix \( U \)
assume as: \( U \in Pow(G) \), \( \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t \in G\}(x) \)
{
fix \( x \)
assume x: \( x\in U \)
with as(1) have xg: \( x\in G \)
from x, as(2) have \( U\in \{\langle t, \{V \{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t \in G\}(x) \)
with xg, fun have \( U\in \{V \{x\} .\ V \in \text{ leftUniformity }\} \) using apply_equality
then obtain \( V \) where V: \( U=V\{x\} \), \( V\in \text{ leftUniformity } \)
from V(2) obtain \( W \) where W: \( W\in \mathcal{N}_0 \), \( \{\langle s,t\rangle :G\times G.\ ( - s) + t:W\}\subseteq V \) unfolding leftUniformity_def
from W(2) have A: \( \{\langle s,t\rangle :G\times G.\ ( - s) + t:W\}\{x\}\subseteq V\{x\} \)
from xg have \( \forall q\in G.\ q\in (\{\langle s,t\rangle :G\times G.\ ( - s) + t:W\}\{x\}) \longleftrightarrow ( - x) + q:W \) using image_iff
hence B: \( \{\langle s,t\rangle :G\times G.\ ( - s) + t:W\}\{x\} = \{t\in G.\ ( - x) + t:W\} \)
from W(1) have WG: \( W\subseteq G \)
{
fix \( t \)
assume t: \( t \in x + W \)
then have \( t \in \text{LeftTranslation}(G,f,x)W \)
then obtain \( s \) where s: \( s\in W \), \( \langle s,t\rangle \in \text{LeftTranslation}(G,f,x) \) using image_iff
with \( W\subseteq G \) have \( s\in G \)
from s(2) have \( t=x + s \), \( t\in G \) unfolding LeftTranslation_def
with \( x\in G \), \( s\in G \) have \( ( - x) + t = s \) using put_on_the_other_side(2)
with s(1) have \( ( - x) + t\in W \)
with \( t\in G \) have \( t \in \{s\in G.\ ( - x) + s:W\} \)
}
then have \( x + W \subseteq \{t\in G.\ ( - x) + t\in W\} \)
with B have \( x + W \subseteq \{\langle s,t\rangle \in G \times G .\ ( - s) + t \in W\} \{x\} \)
with A have \( x + W \subseteq V \{x\} \)
with V(1) have \( x + W \subseteq U \)
then have \( int(x + W) \subseteq U \) using Top_2_L1
moreover
from xg, W(1) have \( x\in int(x + W) \) using elem_in_int_ltrans(1)
moreover
have \( int(x + W)\in T \) using Top_2_L2
ultimately have \( \exists Y\in T.\ x\in Y \wedge Y\subseteq U \)
}
then have \( U\in T \) using open_neigh_open
}
hence \( \{U \in Pow(G) .\ \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t \in G\} x\} \subseteq T \)
moreover {
fix \( U \)
assume as: \( U \in Pow(G) \), \( \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{ rightUniformity }\}\rangle .\ t \in G\} x \)
{
fix \( x \)
assume x: \( x\in U \)
with as(1) have xg: \( x\in G \)
from x, as(2) have \( U\in \{\langle t, \{V \{t\} .\ V \in \text{ rightUniformity }\}\rangle .\ t \in G\} x \)
with xg, funN have \( U\in \{V \{x\} .\ V \in \text{ rightUniformity }\} \) using apply_equality
then obtain \( V \) where V: \( U=V\{x\} \), \( V \in \text{ rightUniformity } \)
then have \( converse(V) \in \text{ rightUniformity } \) using side_uniformities(2) , IsUniformity_def
then obtain \( W \) where W: \( W\in \mathcal{N}_0 \), \( \{\langle s,t\rangle :G\times G.\ s + ( - t):W\}\subseteq converse(V) \) unfolding rightUniformity_def
from W(2) have A: \( \{\langle s,t\rangle :G\times G.\ s + ( - t):W\}^{-1}\{x\}\subseteq V\{x\} \)
from xg have \( \forall q\in G.\ q\in (\{\langle s,t\rangle :G\times G.\ s + ( - t):W\}^{-1}\{x\}) \longleftrightarrow q + ( - x):W \) using image_iff
hence B: \( \{\langle s,t\rangle :G\times G.\ s + ( - t):W\}^{-1}\{x\} = \{t\in G.\ t + ( - x):W\} \)
from W(1) have WG: \( W\subseteq G \)
{
fix \( t \)
assume \( t \in W + x \)
with \( x\in G \), \( W\subseteq G \) obtain \( s \) where \( s\in W \) and \( t=s + x \) using lrtrans_image(2)
with \( W\subseteq G \) have \( s\in G \)
with \( x\in G \), \( t=s + x \) have \( t\in G \) using group_op_closed_add
from \( x\in G \), \( s\in G \), \( t=s + x \) have \( t + ( - x) = s \) using put_on_the_other_side
with \( s\in W \), \( t\in G \) have \( t \in \{s\in G.\ s + ( - x) \in W\} \)
}
then have \( W + x \subseteq \{t:G.\ t + ( - x):W\} \)
with B have \( W + x \subseteq \{\langle s,t\rangle \in G \times G .\ s + ( - t) \in W\}^{-1}\{x\} \)
with A have \( W + x \subseteq V \{x\} \)
with V(1) have \( W + x \subseteq U \)
then have \( int(W + x) \subseteq U \) using Top_2_L1
moreover
from xg, W(1) have \( x\in int(W + x) \) using elem_in_int_rtrans(1)
moreover
have \( int(W + x)\in T \) using Top_2_L2
ultimately have \( \exists Y\in T.\ x\in Y \wedge Y\subseteq U \)
}
then have \( U\in T \) using open_neigh_open
} ultimately have \( \{U \in Pow(G).\ \forall x\in U.\ U \in \{\langle t, \{V\{t\} .\ V \in \text{ leftUniformity }\}\rangle .\ t \in G\}(x)\} = T \), \( \{U \in Pow(G).\ \forall x\in U.\ U \in \{\langle t, \{V\{t\} .\ V \in \text{ rightUniformity }\}\rangle .\ t \in G\}(x)\} = T \)
then show \( \text{UniformTopology}(\text{ leftUniformity },G) = T \) and \( \text{UniformTopology}(\text{ rightUniformity },G) = T \) unfolding UniformTopology_def
qed

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\in G \)

shows \( \text{LeftTranslation}(G,f,x) \text{ is uniformly continuous between } \text{ leftUniformity }\text{ and } \text{ leftUniformity } \)proof
let \( P = \text{ProdFunction}( \text{LeftTranslation}(G, f, x), \text{LeftTranslation}(G, f, x)) \)
from assms have L: \( \text{LeftTranslation}(G,f,x):G\rightarrow G \) and \( \text{ leftUniformity } \text{ is a uniformity on } G \) using group0_5_L1 , side_uniformities(1)
moreover
have \( \forall V \in \text{ leftUniformity }.\ P^{-1}(V) \in \text{ leftUniformity } \)proof
{
fix \( V \)
assume \( V \in \text{ leftUniformity } \)
then obtain \( U \) where \( U \in \mathcal{N}_0 \) and \( \{\langle s,t\rangle \in G \times G .\ ( - s) + t \in U\} \subseteq V \) unfolding leftUniformity_def
with \( V \in \text{ leftUniformity } \) have as: \( V \subseteq G \times G \), \( U \in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G \times G .\ ( - s) + t \in U\} \subseteq V \) unfolding leftUniformity_def
{
fix \( z \)
assume z: \( z \in \{\langle s,t\rangle \in G \times G .\ ( - s) + t \in U\} \)
then obtain \( s \) \( t \) where st: \( z=\langle s,t\rangle \), \( s\in G \), \( t\in G \)
from st(1), z have st2: \( ( - s) + t \in U \)
from assms, st have \( P(z) = \langle \text{LeftTranslation}(G, f, x)(s), \text{LeftTranslation}(G, f, x)(t)\rangle \) using prodFunctionApp , group0_5_L1(2)
with assms, st(2,3) have \( P(z) = \langle x + s,x + t\rangle \) using group0_5_L2(2)
moreover
from \( x\in G \), \( s\in G \), \( t\in G \) have \( ( - (x + s)) + (x + t) = ( - s) + t \) using cancel_middle_add(3)
with st2 have \( ( - (x + s)) + (x + t) \in U \)
ultimately have \( P(z) \in \{\langle s,t\rangle \in G \times G .\ ( - s) + t \in U\} \) using assms , st(2,3) , group_op_closed
with as(3) have \( P(z) \in V \)
with L, z have \( z \in P^{-1}(V) \) using prodFunction , func1_1_L5A , vimage_iff
}
with as(2) have \( \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G \times G .\ ( - s) + t \in U\} \subseteq P^{-1}(V) \)
with \( \text{LeftTranslation}(G,f,x):G\rightarrow G \), \( V \subseteq G \times G \) have \( P^{-1}(V) \in \text{ leftUniformity } \) unfolding leftUniformity_def using prodFunction , func1_1_L6A
}
thus \( thesis \)
qed
ultimately show \( thesis \) using IsUniformlyCont_def
qed

Right translations are uniformly continuous with respect to the right uniformity.

lemma (in topgroup) right_mult_uniformity:

assumes \( x\in G \)

shows \( \text{RightTranslation}(G,f,x) \text{ is uniformly continuous between } \text{ rightUniformity }\text{ and } \text{ rightUniformity } \)proof
let \( P = \text{ProdFunction}( \text{RightTranslation}(G, f, x), \text{RightTranslation}(G, f, x)) \)
from assms have R: \( \text{RightTranslation}(G,f,x):G\rightarrow G \) and \( \text{ rightUniformity } \text{ is a uniformity on } G \) using group0_5_L1 , side_uniformities(2)
moreover
have \( \forall V \in \text{ rightUniformity }.\ P^{-1}(V) \in \text{ rightUniformity } \)proof
{
fix \( V \)
assume \( V \in \text{ rightUniformity } \)
then obtain \( U \) where \( U \in \mathcal{N}_0 \) and \( \{\langle s,t\rangle \in G \times G .\ s + ( - t) \in U\} \subseteq V \) unfolding rightUniformity_def
with \( V \in \text{ rightUniformity } \) have as: \( V \subseteq G \times G \), \( U \in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G \times G .\ s + ( - t) \in U\} \subseteq V \) unfolding rightUniformity_def
{
fix \( z \)
assume z: \( z \in \{\langle s,t\rangle \in G \times G .\ s + ( - t) \in U\} \)
then obtain \( s \) \( t \) where st: \( z=\langle s,t\rangle \), \( s\in G \), \( t\in G \)
from st(1), z have st2: \( s + ( - t) \in U \)
from assms, st have \( P(z) = \langle \text{RightTranslation}(G, f, x)(s), \text{RightTranslation}(G, f, x)(t)\rangle \) using prodFunctionApp , group0_5_L1(1)
with assms, st(2,3) have \( P(z) = \langle s + x,t + x\rangle \) using group0_5_L2(1)
moreover
from \( x\in G \), \( s\in G \), \( t\in G \) have \( (s + x) + ( - (t + x)) =s + ( - t) \) using cancel_middle_add(4)
with st2 have \( (s + x) + ( - (t + x)) \in U \)
ultimately have \( P(z) \in \{\langle s,t\rangle \in G \times G .\ s + ( - t) \in U\} \) using assms , st(2,3) , group_op_closed
with as(3) have \( P(z) \in V \)
with R, z have \( z \in P^{-1}(V) \) using prodFunction , func1_1_L5A , vimage_iff
}
with as(2) have \( \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G \times G .\ s + ( - t) \in U\} \subseteq P^{-1}(V) \)
with \( \text{RightTranslation}(G,f,x):G\rightarrow G \), \( V \subseteq G \times G \) have \( P^{-1}(V) \in \text{ rightUniformity } \) unfolding rightUniformity_def using prodFunction , func1_1_L6A
}
thus \( thesis \)
qed
ultimately show \( thesis \) using IsUniformlyCont_def
qed

The third uniformity important on topological groups is called the uniformity of Roelcke.

Definition (in topgroup)

\( \text{roelckeUniformity} \equiv \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ t \in (U + s) + U\}\subseteq V\} \)

The Roelcke uniformity is indeed a uniformity on the group.

lemma (in topgroup) roelcke_uniformity:

shows \( \text{roelckeUniformity} \text{ is a uniformity on } G \)proof
let \( \Phi = \text{roelckeUniformity} \)
have \( \forall U \in \Phi .\ id(G)\subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi \)proof
fix \( U \)
assume U: \( U \in \text{roelckeUniformity} \)
then obtain \( V \) where V: \( \{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\} \subseteq U \), \( V\in \mathcal{N}_0 \), \( U:Pow(G\times G) \) unfolding roelckeUniformity_def
from V(2) have VG: \( V\subseteq G \)
have \( id(G) \subseteq U \)proof
from V(2) have \( 0 \in int(V) \)
then have V0: \( 0 \in V \) using Top_2_L1
{
fix \( x \)
assume x: \( x\in G \)
with \( V\in \mathcal{N}_0 \) have \( x \in V + x \) using elem_in_int_rtrans(1) , Top_2_L1
with \( V\subseteq G \), \( x\in G \), \( 0 \in V \) have \( x + 0 : (V + x) + V \) using lrtrans_in_group_add(2) , interval_add(4)
with \( x\in G \) have \( x: (V + x) + V \) using group0_2_L2
with \( x\in G \) have \( \langle x,x\rangle :\{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\} \)
with V(1) have \( \langle x,x\rangle \in U \)
}
thus \( id(G) \subseteq U \)
qed
moreover
have \( converse(U) \in \Phi \)proof
{
fix \( l \)
assume \( l \in \{\langle s,t\rangle \in G\times G.\ t \in ((-V) + s) + (-V)\} \)
then obtain \( s \) \( t \) where st: \( s\in G \), \( t\in G \), \( t \in ((-V) + s) + (-V) \), \( l=\langle s,t\rangle \)
from \( V\subseteq G \) have smG: \( (-V) \subseteq G \) using ginv_image_add(1)
with \( s\in G \) have VxG: \( (-V) + s \subseteq G \) using lrtrans_in_group_add(2)
from \( V\subseteq G \), \( t\in G \) have VsG: \( V + t \subseteq G \) using lrtrans_in_group_add(2)
from st(3), VxG, smG obtain \( x \) \( y \) where xy: \( t = x + y \), \( x \in (-V) + s \), \( y\in (-V) \) using elements_in_set_sum
from xy(2), smG, st(1) obtain \( z \) where z: \( x = z + s \), \( z\in (-V) \) using elements_in_rtrans
with \( y\in (-V) \), \( (-V)\subseteq G \), \( s\in G \), \( t = x + y \) have ts: \( ( - z) + t + ( - y) = s \) using cancel_middle_add(5)
{
fix \( u \)
assume \( u\in (-V) \)
with \( V\subseteq G \) have \( ( - u) \in V \) using ginv_image_el_add
}
hence R: \( \forall u\in (-V).\ ( - u) \in V \)
with z(2), xy(3) have zy: \( ( - z)\in V \), \( ( - y)\in V \)
from zy(1), VG, st(2) have \( ( - z) + t : V + t \) using lrtrans_image(2)
with zy(2), VG, VsG have \( ( - z) + t + ( - y) : (V + t) + V \) using interval_add(4)
with ts have \( s:(V + t) + V \)
with st(1,2) have \( \langle s,t\rangle \in converse(\{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\}) \) using converse_iff
with V(1) have \( \langle s,t\rangle \in converse(U) \)
with st(4) have \( l \in converse(U) \)
}
then have \( \{\langle s,t\rangle \in G\times G.\ t \in ((-V) + s) + (-V)\} \subseteq converse(U) \)
moreover
from V(2) have \( (-V): \mathcal{N}_0 \) using neg_neigh_neigh
ultimately have \( \exists V\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\} \subseteq converse(U) \)
moreover
from V(3) have \( converse(U) \subseteq G\times G \) unfolding converse_def
ultimately show \( converse(U) \in \text{roelckeUniformity} \) unfolding roelckeUniformity_def
qed
moreover
have \( \exists Z\in \Phi .\ Z\circ Z \subseteq U \)proof
from V(2) obtain \( W \) where W: \( W\in \mathcal{N}_0 \), \( W + W \subseteq V \) using exists_procls_zerohood
then have WG: \( W\subseteq G \)
moreover {
fix \( k \)
assume as: \( k:\{\langle s,t\rangle \in G\times G.\ t \in (W + s) + W\}\circ \{\langle s,t\rangle \in G\times G.\ t \in (W + s) + W\} \)
then obtain \( x_1 \) \( x_2 \) \( x_3 \) where x: \( x_1\in G \), \( x_2\in G \), \( x_3\in G \), \( x_2 \in (W + x_1) + W \), \( x_3 \in (W + x_2) + W \), \( k=\langle x_1,x_3\rangle \) unfolding comp_def
from \( x_1\in G \) have VsG: \( W + x_1 \subseteq G \) and Vx1G: \( V + x_1 \subseteq G \) using lrtrans_in_group_add(2)
from x(4), VsG, WG obtain \( x \) \( y \) where xy: \( x_2 = x + y \), \( x \in W + x_1 \), \( y\in W \) using elements_in_set_sum
from xy(2), WG, x(1) obtain \( z \) where z: \( x = z + x_1 \), \( z\in W \) using elements_in_rtrans
from z(2), xy(3), WG have yzG: \( y\in G \), \( z\in G \)
from x(2) have VsG: \( W + x_2 \subseteq G \) using lrtrans_in_group_add
from x(5), VsG, WG obtain \( x' \) \( y' \) where xy2: \( x_3 = x' + y' \), \( x'\in W + x_2 \), \( y'\in W \) using elements_in_set_sum
from xy2(2), WG, x(2) obtain \( z' \) where z2: \( x' = z' + x_2 \), \( z'\in W \) using elements_in_rtrans
from z2(2), xy2(3), WG have yzG2: \( y'\in G \), \( z'\in G \)
from xy(1), z(1), xy2(1), z2(1) have \( x_3 = (z' + (z + x_1 + y)) + y' \)
with yzG, yzG2, x(1) have x3: \( x_3 = ((z' + z) + x_1) + (y + y') \) using group_oper_assoc , group_op_closed
from xy(3), z(2), xy2(3), z2(2), WG have \( z' + z \in W + W \), \( y + y' \in W + W \) using interval_add(4)
with W(2) have yzV: \( z' + z \in V \), \( y + y' \in V \)
from yzV(1), VG, x(1) have \( (z' + z) + x_1 \in V + x_1 \) using lrtrans_image(2)
with yzV(2), Vx1G, VG have \( ((z' + z) + x_1) + (y + y') \in (V + x_1) + V \) using interval_add(4)
with x3 have \( x_3 \in (V + x_1) + V \)
with x(1,3,6) have \( k:\{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\} \)
}
with V(1) have \( \{\langle s,t\rangle \in G\times G.\ t \in (W + s) + W\}\circ \{\langle s,t\rangle \in G\times G.\ t \in (W + s) + W\}\subseteq U \)
moreover
from W(1) have \( \{\langle s,t\rangle \in G\times G.\ t \in (W + s) + W\}\in \text{roelckeUniformity} \) unfolding roelckeUniformity_def
ultimately show \( \exists Z\in \text{roelckeUniformity}.\ Z\circ Z \subseteq U \)
qed
ultimately show \( id(G)\subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi \)
qed
moreover
have \( \text{roelckeUniformity} \text{ is a filter on } (G \times G) \)proof
{
assume \( 0 \in \text{roelckeUniformity} \)
then obtain \( W \) where U: \( W\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ t \in (W + s) + W\}\subseteq 0 \) unfolding roelckeUniformity_def
have \( \langle 0 , 0 \rangle :G\times G \) using zero_in_tgroup
moreover
have \( 0 = 0 + 0 + 0 \) using group0_2_L2 , zero_in_tgroup
moreover
from U(1) have \( 0 \in int(W) \)
then have \( 0 \in W \) using Top_2_L1
with \( W\in \mathcal{N}_0 \) have \( 0 + 0 + 0 \in (W + 0 ) + W \) using group0_2_L2 , group_op_closed , trans_neutral_image , interval_add_zero
ultimately have \( \langle 0 , 0 \rangle \in \{\langle s,t\rangle \in G\times G.\ t \in (W + s) + W\} \)
with U(2) have \( False \)
}
moreover {
fix \( x \) \( xa \)
assume as: \( x \in \text{roelckeUniformity} \), \( xa\in x \)
have \( \text{roelckeUniformity} \subseteq Pow(G\times G) \) unfolding roelckeUniformity_def
with as have \( xa \in G\times G \)
} moreover {
have \( G\times G\in Pow(G\times G) \)
moreover
have \( \{\langle s,t\rangle :G\times G.\ t \in (G + s) + G\} \subseteq G\times G \)
moreover
note zneigh_not_empty
ultimately have \( G\times G\in \text{roelckeUniformity} \) unfolding roelckeUniformity_def
} moreover {
fix \( A \) \( B \)
assume as: \( A\in \text{roelckeUniformity} \), \( B\in \text{roelckeUniformity} \)
from as(1) obtain \( AU \) where AU: \( AU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ t \in (AU + s) + AU\}\subseteq A \), \( A\in Pow(G\times G) \) unfolding roelckeUniformity_def
from as(2) obtain \( BU \) where BU: \( BU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ t \in (BU + s) + BU\}\subseteq B \), \( B\in Pow(G\times G) \) unfolding roelckeUniformity_def
from AU(1), BU(1) have \( 0 \in int(AU)\cap int(BU) \)
moreover
have op: \( int(AU)\cap int(BU)\in T \) using Top_2_L2 , topSpaceAssum unfolding IsATopology_def
moreover
have \( int(AU)\cap int(BU) \subseteq AU\cap BU \) using Top_2_L1
with op have \( int(AU)\cap int(BU)\subseteq int(AU\cap BU) \) using Top_2_L5
moreover
note AU(1), BU(1)
ultimately have interNeigh: \( AU\cap BU \in \mathcal{N}_0 \) unfolding zerohoods_def
moreover {
fix \( z \)
assume \( z \in \{\langle s,t\rangle \in G\times G.\ t \in ((AU\cap BU) + s) + (AU\cap BU)\} \)
then obtain \( s \) \( t \) where z: \( z=\langle s,t\rangle \), \( s\in G \), \( t\in G \), \( t \in ((AU\cap BU) + s) + (AU\cap BU) \)
from \( AU\cap BU \in \mathcal{N}_0 \), \( s\in G \) have \( AU\cap BU \subseteq G \) and \( (AU\cap BU) + s \subseteq G \) using lrtrans_in_group_add(2)
with z(4) obtain \( x \) \( y \) where t: \( t=x + y \), \( x\in (AU\cap BU) + s \), \( y\in AU\cap BU \) using elements_in_set_sum
from t(2), z(2), interNeigh obtain \( q \) where x: \( x=q + s \), \( q \in AU\cap BU \) using lrtrans_image(2)
with AU(1), BU(1), z(2) have \( x \in AU + s \), \( x \in BU + s \) using lrtrans_image(2)
with \( y \in AU\cap BU \), \( AU\in \mathcal{N}_0 \), \( BU\in \mathcal{N}_0 \), \( s \in G \), \( t=x + y \) have \( t \in (AU + s) + AU \) and \( t \in (BU + s) + BU \) using lrtrans_in_group_add(2) , elements_in_set_sum_inv
with z(1,2,3) have \( z \in \{\langle s,t\rangle \in G\times G.\ t \in (AU + s) + AU\} \) and \( z \in \{\langle s,t\rangle \in G\times G.\ t \in (BU + s) + BU\} \)
}
then have \( \{\langle s,t\rangle \in G\times G.\ t \in ((AU\cap BU) + s) + (AU\cap BU)\} \subseteq \) \( \{\langle s,t\rangle \in G\times G.\ t \in (AU + s) + AU\}\cap \{\langle s,t\rangle \in G\times G.\ t \in (BU + s) + BU\} \)
with AU(2), BU(2) have \( \{\langle s,t\rangle \in G\times G.\ t \in ((AU\cap BU) + s) + (AU\cap BU)\}\subseteq A\cap B \)
ultimately have \( A\cap B \in \text{roelckeUniformity} \) using AU(3) , BU(3) unfolding roelckeUniformity_def
} moreover {
fix \( B \) \( C \)
assume as: \( B\in \text{roelckeUniformity} \), \( C\subseteq (G \times G) \), \( B \subseteq C \)
from as(1) obtain \( BU \) where BU: \( BU\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ t \in (BU + s) + BU\}\subseteq B \) unfolding roelckeUniformity_def
from as(3), BU(2) have \( \{\langle s,t\rangle \in G\times G.\ t \in (BU + s) + BU\}\subseteq C \)
then have \( C \in \text{roelckeUniformity} \) using as(2) , BU(1) unfolding roelckeUniformity_def
} ultimately show \( thesis \) unfolding IsFilter_def
qed
ultimately show \( thesis \) using IsUniformity_def
qed

The topology given by the roelcke uniformity is the original topology

lemma (in topgroup) top_generated_roelcke_uniformity:

shows \( \text{UniformTopology}(\text{roelckeUniformity},G) = T \)proof
let \( M = \{\langle t, \{V \{t\} .\ V \in \text{roelckeUniformity}\}\rangle .\ t \in G\} \)
have fun: \( M:G\rightarrow Pow(Pow(G)) \) using IsNeighSystem_def , neigh_from_uniformity , roelcke_uniformity
{
fix \( U \)
assume as: \( U \in \{U \in Pow(G).\ \forall x\in U.\ U \in Mx\} \)
{
fix \( x \)
assume x: \( x\in U \)
with as have xg: \( x\in G \)
from x, as have \( U \in \{\langle t, \{V \{t\} .\ V \in \text{roelckeUniformity}\}\rangle .\ t \in G\}(x) \)
with fun, \( x\in G \) have \( U \in \{V \{x\} .\ V \in \text{roelckeUniformity}\} \) using ZF_fun_from_tot_val
then obtain \( V \) where V: \( U=V\{x\} \), \( V \in \text{roelckeUniformity} \)
from V(2) obtain \( W \) where W: \( W\in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G\times G.\ t\in (W + s) + W\}\subseteq V \) unfolding roelckeUniformity_def
from W(1) have WG: \( W\subseteq G \)
from W(2) have A: \( \{\langle s,t\rangle :G\times G.\ t:(W + s) + W\}\{x\} \subseteq V\{x\} \)
have \( \{\langle s,t\rangle \in G\times G.\ t \in (W + s) + W\}\{x\} = (W + x) + W \)proof
let \( A = \{\langle s,t\rangle :G\times G.\ t \in (W + s) + W\} \)
from \( W\subseteq G \), \( x\in G \) have I: \( (W + x) + W \subseteq G \) using lrtrans_in_group_add , interval_add(1)
have \( A\{x\} = \{t\in G.\ \langle x,t\rangle \in A\} \)
moreover
have \( \{t\in G.\ \langle x,t\rangle \in A\} \subseteq (W + x) + W \)
moreover
from \( W\subseteq G \), \( x\in G \), I have \( (W + x) + W \subseteq \{t\in G.\ \langle x,t\rangle \in A\} \)
ultimately show \( thesis \)
qed
with A, V(1) have WU: \( (W + x) + W \subseteq U \)
have \( int(W) + x \subseteq W + x \) using image_mono , Top_2_L1
then have \( (int(W) + x)\times (int(W)) \subseteq (W + x)\times W \) using Top_2_L1
then have \( f((int(W) + x)\times (int(W))) \subseteq f((W + x)\times W) \) using image_mono
moreover
from xg, WG have \( \langle int(W) + x,int(W)\rangle \in Pow(G)\times Pow(G) \) and \( \langle (W + x),W\rangle \in Pow(G)\times Pow(G) \) using Top_2_L2 , lrtrans_in_group_add(2)
then have \( (int(W) + x) + (int(W)) = f((int(W) + x)\times (int(W))) \) and \( (W + x) + W = f((W + x)\times W) \) using interval_add(2)
ultimately have \( (int(W) + x) + (int(W)) \subseteq (W + x) + W \)
with xg, WG have \( int(W + x) + (int(W)) \subseteq (W + x) + W \) using rtrans_interior
moreover {
have \( int(W + x) + (int(W)) = (\bigcup t\in int(W + x).\ t + (int(W))) \) using interval_add(3) , Top_2_L2
moreover
have \( \forall t\in int(W + x).\ t + (int(W)) = int(t + W) \)proof
{
fix \( t \)
assume \( t \in int(W + x) \)
from \( x\in G \) have \( (W + x) \subseteq G \) using lrtrans_in_group_add(2)
with \( t \in int(W + x) \) have \( t\in G \) using Top_2_L2
with \( W\subseteq G \) have \( t + int(W) = int(t + W) \) using ltrans_interior
}
thus \( thesis \)
qed
ultimately have \( int(W + x) + (int(W)) = (\bigcup t\in int(W + x).\ int(t + W)) \)
with topSpaceAssum have \( int(W + x) + (int(W)) \in T \) using Top_2_L2 , union_open
} moreover
from \( x\in G \), \( W\in \mathcal{N}_0 \) have \( x \in int(W + x) + (int(W)) \) using elem_in_int_rtrans(2)
moreover
note WU
ultimately have \( \exists Y\in T.\ x\in Y \wedge Y\subseteq U \)
}
then have \( U\in T \) using open_neigh_open
}
then have \( \{U \in Pow(G).\ \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{roelckeUniformity}\}\rangle .\ t \in G\}(x)\} \subseteq T \)
moreover {
fix \( U \)
assume op: \( U\in T \)
{
fix \( x \)
assume x: \( x\in U \)
with op have xg: \( x\in G \)
have \( ( - x) + U \in \mathcal{N}_0 \) using open_trans_neigh , op , x
then obtain \( W \) where W: \( W\in \mathcal{N}_0 \), \( W + W \subseteq ( - x) + U \) using exists_procls_zerohood
let \( V = x + (W + ( - x)) \cap W \)
from \( W \in \mathcal{N}_0 \), \( x\in G \) have xWx: \( x + (W + ( - x)) :\mathcal{N}_0 \) using lrtrans_neigh
from W(1) have WG: \( W\subseteq G \)
from xWx, W(1) have \( 0 \in int(x + (W + ( - x)))\cap int(W) \)
have int: \( int(x + (W + ( - x)))\cap int(W)\in T \) using Top_2_L2 , topSpaceAssum unfolding IsATopology_def
have \( int(x + (W + ( - x)))\cap int(W) \subseteq (x + (W + ( - x)))\cap W \) using Top_2_L1
with int have \( int(x + (W + ( - x)))\cap int(W)\subseteq int((x + (W + ( - x)))\cap W) \) using Top_2_L5
moreover
note xWx, W(1)
ultimately have V_NEIG: \( V \in \mathcal{N}_0 \) unfolding zerohoods_def
{
fix \( z \)
assume z: \( z \in (V + x) + V \)
from W(1) have VG: \( V \subseteq G \)
with \( x\in G \) have VxG: \( V + x \subseteq G \) using lrtrans_in_group_add(2)
from z, VG, VxG, W(1) obtain \( a_1 \) \( b_1 \) where ab: \( z=a_1 + b_1 \), \( a_1 \in V + x \), \( b_1 \in V \) using elements_in_set_sum
from ab(2), xg, VG obtain \( c_1 \) where c: \( a_1=c_1 + x \), \( c_1 \in V \) using elements_in_rtrans
from ab(3), c(2) have bc: \( b_1\in W \), \( c_1 \in x + (W + ( - x)) \)
from \( x\in G \) have \( x + (W + ( - x)) = \{x + y.\ y\in (W + ( - x))\} \) using neg_in_tgroup , lrtrans_in_group_add , lrtrans_image
with \( c_1 \in x + (W + ( - x)) \) obtain \( d \) where d: \( c_1=x + d \), \( d \in W + ( - x) \)
from \( x\in G \), \( W\in \mathcal{N}_0 \), \( d \in W + ( - x) \) obtain \( e \) where e: \( d=e + ( - x) \), \( e\in W \) using neg_in_tgroup , lrtrans_in_group , lrtrans_image(2)
from e(2), WG have eG: \( e\in G \)
from \( e\in W \), \( W\subseteq G \), \( b_1\in W \) have \( e\in G \), \( b_1\in G \)
from \( z = a_1 + b_1 \), \( a_1 = c_1 + x \), \( c_1 = x + d \), \( d = e + ( - x) \) have \( z = x + (e + ( - x)) + x + b_1 \)
with \( x\in G \), \( e\in G \) have \( z=(x + e) + b_1 \) using cancel_middle(4)
with \( x\in G \), \( e\in G \), \( b_1\in G \) have \( z = x + (e + b_1) \) using group_oper_assoc
moreover
from e(2), ab(3), WG have \( e + b_1 \in W + W \) using elements_in_set_sum_inv
moreover
note xg, WG
ultimately have \( z\in x + (W + W) \) using elements_in_ltrans_inv , interval_add(1)
moreover
from \( W\subseteq G \), \( U\in T \) have \( W + W \subseteq G \) and \( U\subseteq G \) using interval_add(1)
with \( W + W \subseteq ( - x) + U \), \( x\in G \) have \( x + (W + W) \subseteq U \) using trans_subset
ultimately have \( z\in U \)
}
then have sub: \( (V + x) + V \subseteq U \)
moreover
from V_NEIG have unif: \( \{\langle s,t\rangle \in G\times G.\ t : (V + s) + V\} \in \text{roelckeUniformity} \) unfolding roelckeUniformity_def
moreover
from xg have \( \forall q.\ q\in \{\langle s,t\rangle \in G\times G.\ t : (V + s) + V\}\{x\} \longleftrightarrow q\in ((V + x) + V)\cap G \)
then have \( \{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\}\{x\} = ((V + x) + V)\cap G \)
ultimately have basic: \( \{\langle s,t\rangle \in G\times G.\ t : (V + s) + V\}\{x\} \subseteq U \) using op
have add: \( (\{x\}\times U)\{x\} =U \)
from basic, add have \( (\{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\}\cup (\{x\}\times U))\{x\} = U \)
moreover
have R: \( \forall B\in \text{roelckeUniformity}.\ (\forall C\in Pow(G \times G).\ B \subseteq C \longrightarrow C \in \text{roelckeUniformity}) \) using roelcke_uniformity unfolding IsUniformity_def , IsFilter_def
moreover
from op, xg have GG: \( (\{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\}\cup (\{x\}\times U)):Pow(G\times G) \)
moreover
have \( \{\langle s,t\rangle \in G\times G.\ t\in (V + s) + V\} \subseteq (\{\langle s,t\rangle \in G\times G.\ t\in (V + s) + V\}\cup (\{x\}\times U)) \)
moreover
from R, unif, GG have \( (\{\langle s,t\rangle \in G\times G.\ t \in (V + s) + V\}\cup (\{x\}\times U)) \in \text{roelckeUniformity} \)
ultimately have \( \exists V\in \text{roelckeUniformity}.\ V\{x\} = U \)
then have \( U \in \{V \{x\} .\ V \in \text{roelckeUniformity}\} \)
with xg, fun have \( U \in \{\langle t, \{V \{t\} .\ V \in \text{roelckeUniformity}\}\rangle .\ t \in G\} x \) using apply_equality
}
hence \( \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{roelckeUniformity}\}\rangle .\ t \in G\} x \)
with op have \( U:\{U \in Pow(G).\ \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{roelckeUniformity}\}\rangle .\ t \in G\}(x)\} \)
}
then have \( T \subseteq \{U \in Pow(G).\ \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{roelckeUniformity}\}\rangle .\ t \in G\}(x)\} \)
ultimately have \( \{U \in Pow(G).\ \forall x\in U.\ U \in \{\langle t, \{V \{t\} .\ V \in \text{roelckeUniformity}\}\rangle .\ t \in G\}(x)\} = T \)
then show \( thesis \) unfolding UniformTopology_def
qed
end
Definition of leftUniformity: \( \text{ leftUniformity } \equiv \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ ( - s) + t \in U\} \subseteq V\} \)
lemma (in topgroup) zero_in_tgroup: shows \( 0 \in G \)
lemma (in topgroup) group0_valid_in_tgroup: shows \( group0(G,f) \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)
Definition of IsATopology: \( T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge \) \( ( \forall U\in T.\ \forall V\in T.\ U\cap V \in T) \)
lemma (in topology0) Top_2_L5:

assumes \( U\subseteq A \) and \( U\in T \)

shows \( U \subseteq int(A) \)
Definition of IsFilter: \( \mathfrak{F} \text{ is a filter on } X \equiv (0\notin \mathfrak{F} ) \wedge (X\in \mathfrak{F} ) \wedge (\mathfrak{F} \subseteq Pow(X)) \wedge \) \( (\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F} ) \wedge (\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} ) \)
Definition of rightUniformity: \( \text{ rightUniformity } \equiv \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ s + ( - t) \in U\}\subseteq V\} \)
lemma (in group0) group0_2_L6:

assumes \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)
lemma (in topgroup) ginv_image_add:

assumes \( V\subseteq G \)

shows \( (-V)\subseteq G \) and \( (-V) = \{ - x.\ x \in V\} \)
lemma (in topgroup) simple_equation1_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \), \( ( - x_1) + x_2 = ( - x_3) \)

shows \( x_3 = ( - x_2) + x_1 \)
lemma (in topgroup) neg_neigh_neigh:

assumes \( H \in \mathcal{N}_0 \)

shows \( (-H) \in \mathcal{N}_0 \)
theorem (in topgroup) exists_procls_zerohood:

assumes \( U\in \mathcal{N}_0 \)

shows \( \exists V\in \mathcal{N}_0.\ (V\subseteq U\wedge (V + V)\subseteq U \wedge (-V)=V) \)
lemma (in topgroup) interval_add:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( A + B \subseteq G \), \( A + B = f(A\times B) \), \( A + B = (\bigcup x\in A.\ x + B) \), \( A + B = \{x + y.\ \langle x,y\rangle \in A\times B\} \)
lemma func_imagedef:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)

shows \( f(A) = \{f(x).\ x \in A\} \)
lemma (in topgroup) topgroup_f_binop: shows \( f : G\times G \rightarrow G \)
lemma (in topgroup) cancel_middle_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \)

shows \( (x_1 + ( - x_2)) + (x_2 + ( - x_3)) = x_1 + ( - x_3) \), \( (( - x_1) + x_2) + (( - x_2) + x_3) = ( - x_1) + x_3 \), \( ( - (x_1 + x_2)) + (x_1 + x_3) = ( - x_2) + x_3 \), \( (x_1 + x_2) + ( - (x_3 + x_2)) =x_1 + ( - x_3) \), \( ( - x_1) + (x_1 + x_2 + x_3) + ( - x_3) = x_2 \)
Definition of IsUniformity: \( \Phi \text{ is a uniformity on } X \equiv (\Phi \text{ is a filter on } (X\times X))\) \( \wedge (\forall U\in \Phi .\ id(X) \subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi ) \)
lemma (in topgroup) simple_equation0_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \), \( x_1 + ( - x_2) = ( - x_3) \)

shows \( x_3 = x_2 + ( - x_1) \)
lemma (in topgroup) cancel_middle_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \)

shows \( (x_1 + ( - x_2)) + (x_2 + ( - x_3)) = x_1 + ( - x_3) \), \( (( - x_1) + x_2) + (( - x_2) + x_3) = ( - x_1) + x_3 \), \( ( - (x_1 + x_2)) + (x_1 + x_3) = ( - x_2) + x_3 \), \( (x_1 + x_2) + ( - (x_3 + x_2)) =x_1 + ( - x_3) \), \( ( - x_1) + (x_1 + x_2 + x_3) + ( - x_3) = x_2 \)
theorem neigh_from_uniformity:

assumes \( \Phi \text{ is a uniformity on } X \)

shows \( \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \text{ is a neighborhood system on } X \)
lemma (in topgroup) side_uniformities: shows \( \text{ leftUniformity } \text{ is a uniformity on } G \) and \( \text{ rightUniformity } \text{ is a uniformity on } G \)
Definition of IsNeighSystem: \( \mathcal{M} \text{ is a neighborhood system on } X \equiv (\mathcal{M} : X\rightarrow Pow(Pow(X))) \wedge \) \( (\forall x\in X.\ (\mathcal{M} (x) \text{ is a filter on } X) \wedge (\forall N\in \mathcal{M} (x).\ x\in N \wedge (\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y)) ) )) \)
lemma (in topgroup) side_uniformities: shows \( \text{ leftUniformity } \text{ is a uniformity on } G \) and \( \text{ rightUniformity } \text{ is a uniformity on } G \)
lemma (in topgroup) neg_in_tgroup:

assumes \( g\in G \)

shows \( ( - g) \in G \)
lemma ZF_fun_from_tot_val:

assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \)
lemma (in topgroup) open_trans_neigh:

assumes \( U\in T \) and \( g\in U \)

shows \( ( - g) + U \in \mathcal{N}_0 \)
Definition of LeftTranslation: \( \text{LeftTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle g,a\rangle = b\} \)
lemma (in topgroup) cancel_left_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \), \( x_1 + x_2 = x_1 + x_3 \)

shows \( x_2 = x_3 \)
lemma (in topgroup) lrtrans_image:

assumes \( V\subseteq G \), \( x\in G \)

shows \( x + V = \{x + v.\ v\in V\} \), \( V + x = \{v + x.\ v\in V\} \)
lemma (in topgroup) open_trans_neigh_2:

assumes \( U\in T \) and \( g\in U \)

shows \( U + ( - g) \in \mathcal{N}_0 \)
Definition of RightTranslation: \( \text{RightTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle a,g\rangle = b\} \)
lemma (in topgroup) cancel_right_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \), \( x_1 + x_2 = x_3 + x_2 \)

shows \( x_1 = x_3 \)
lemma (in topgroup) lrtrans_image:

assumes \( V\subseteq G \), \( x\in G \)

shows \( x + V = \{x + v.\ v\in V\} \), \( V + x = \{v + x.\ v\in V\} \)
lemma (in topgroup) put_on_the_other_side:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 = x_1 + x_2 \)

shows \( x_3 + ( - x_2) = x_1 \) and \( ( - x_1) + x_3 = x_2 \)
lemma (in topgroup) elem_in_int_ltrans:

assumes \( g\in G \) and \( H \in \mathcal{N}_0 \)

shows \( g \in int(g + H) \) and \( g \in int(g + H) + int(H) \)
lemma (in topology0) open_neigh_open:

assumes \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)

shows \( V\in T \)
lemma (in topgroup) group_op_closed_add:

assumes \( x_1 \in G \), \( x_2 \in G \)

shows \( x_1 + x_2 \in G \)
lemma (in topgroup) put_on_the_other_side:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 = x_1 + x_2 \)

shows \( x_3 + ( - x_2) = x_1 \) and \( ( - x_1) + x_3 = x_2 \)
lemma (in topgroup) elem_in_int_rtrans:

assumes \( g\in G \) and \( H \in \mathcal{N}_0 \)

shows \( g \in int(H + g) \) and \( g \in int(H + g) + int(H) \)
Definition of UniformTopology: \( \text{UniformTopology}(\Phi ,X) \equiv \{U \in Pow(X).\ \forall x\in U.\ U \in \{\langle t,\{V\{t\}.\ V\in \Phi \}\rangle .\ t\in X\}(x)\} \)
lemma (in group0) group0_5_L1:

assumes \( g\in G \)

shows \( \text{RightTranslation}(G,P,g) : G\rightarrow G \) and \( \text{LeftTranslation}(G,P,g) : G\rightarrow G \)
lemma prodFunctionApp:

assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \), \( x\in A \), \( y\in C \)

shows \( \text{ProdFunction}(f,g)\langle x,y\rangle = \langle f(x),g(y)\rangle \)
lemma (in group0) group0_5_L1:

assumes \( g\in G \)

shows \( \text{RightTranslation}(G,P,g) : G\rightarrow G \) and \( \text{LeftTranslation}(G,P,g) : G\rightarrow G \)
lemma (in group0) group0_5_L2:

assumes \( g\in G \), \( a\in G \)

shows \( \text{RightTranslation}(G,P,g)(a) = a\cdot g \), \( \text{LeftTranslation}(G,P,g)(a) = g\cdot a \)
lemma (in topgroup) cancel_middle_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \)

shows \( (x_1 + ( - x_2)) + (x_2 + ( - x_3)) = x_1 + ( - x_3) \), \( (( - x_1) + x_2) + (( - x_2) + x_3) = ( - x_1) + x_3 \), \( ( - (x_1 + x_2)) + (x_1 + x_3) = ( - x_2) + x_3 \), \( (x_1 + x_2) + ( - (x_3 + x_2)) =x_1 + ( - x_3) \), \( ( - x_1) + (x_1 + x_2 + x_3) + ( - x_3) = x_2 \)
lemma (in group0) group_op_closed:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b \in G \)
lemma prodFunction:

assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \)

shows \( \text{ProdFunction}(f,g):(A\times C)\rightarrow (B\times D) \)
lemma func1_1_L5A:

assumes \( f:X\rightarrow Y \), \( x\in X \), \( y = f(x) \)

shows \( \langle x,y\rangle \in f \), \( y \in \text{range}(f) \)
lemma func1_1_L6A:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A)\subseteq X \)
Definition of IsUniformlyCont: \( f:X->Y ==> \Phi \text{ is a uniformity on }X ==> \Gamma \text{ is a uniformity on }Y ==> \) \( f \text{ is uniformly continuous between } \Phi \text{ and } \Gamma \equiv \forall V\in \Gamma .\ ( \text{ProdFunction}(f,f)^{-1}V)\in \Phi \)
lemma (in group0) group0_5_L1:

assumes \( g\in G \)

shows \( \text{RightTranslation}(G,P,g) : G\rightarrow G \) and \( \text{LeftTranslation}(G,P,g) : G\rightarrow G \)
lemma (in group0) group0_5_L2:

assumes \( g\in G \), \( a\in G \)

shows \( \text{RightTranslation}(G,P,g)(a) = a\cdot g \), \( \text{LeftTranslation}(G,P,g)(a) = g\cdot a \)
lemma (in topgroup) cancel_middle_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \)

shows \( (x_1 + ( - x_2)) + (x_2 + ( - x_3)) = x_1 + ( - x_3) \), \( (( - x_1) + x_2) + (( - x_2) + x_3) = ( - x_1) + x_3 \), \( ( - (x_1 + x_2)) + (x_1 + x_3) = ( - x_2) + x_3 \), \( (x_1 + x_2) + ( - (x_3 + x_2)) =x_1 + ( - x_3) \), \( ( - x_1) + (x_1 + x_2 + x_3) + ( - x_3) = x_2 \)
Definition of roelckeUniformity: \( \text{roelckeUniformity} \equiv \{V\in Pow(G\times G).\ \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G\times G.\ t \in (U + s) + U\}\subseteq V\} \)
lemma (in topgroup) lrtrans_in_group_add:

assumes \( x\in G \)

shows \( x + V \subseteq G \) and \( V + x \subseteq G \)
lemma (in topgroup) interval_add:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( A + B \subseteq G \), \( A + B = f(A\times B) \), \( A + B = (\bigcup x\in A.\ x + B) \), \( A + B = \{x + y.\ \langle x,y\rangle \in A\times B\} \)
lemma (in topgroup) ginv_image_add:

assumes \( V\subseteq G \)

shows \( (-V)\subseteq G \) and \( (-V) = \{ - x.\ x \in V\} \)
corollary (in topgroup) elements_in_set_sum:

assumes \( A\subseteq G \), \( B\subseteq G \), \( t \in A + B \)

shows \( \exists s\in A.\ \exists q\in B.\ t=s + q \)
corollary (in topgroup) elements_in_rtrans:

assumes \( B\subseteq G \), \( g\in G \), \( t \in B + g \)

shows \( \exists q\in B.\ t=q + g \)
lemma (in topgroup) cancel_middle_add:

assumes \( x_1 \in G \), \( x_2 \in G \), \( x_3 \in G \)

shows \( (x_1 + ( - x_2)) + (x_2 + ( - x_3)) = x_1 + ( - x_3) \), \( (( - x_1) + x_2) + (( - x_2) + x_3) = ( - x_1) + x_3 \), \( ( - (x_1 + x_2)) + (x_1 + x_3) = ( - x_2) + x_3 \), \( (x_1 + x_2) + ( - (x_3 + x_2)) =x_1 + ( - x_3) \), \( ( - x_1) + (x_1 + x_2 + x_3) + ( - x_3) = x_2 \)
lemma (in topgroup) ginv_image_el_add:

assumes \( V\subseteq G \), \( x \in (-V) \)

shows \( ( - x) \in V \)
lemma (in topgroup) lrtrans_in_group_add:

assumes \( x\in G \)

shows \( x + V \subseteq G \) and \( V + x \subseteq G \)
lemma (in group0) group_oper_assoc:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot (b\cdot c) = a\cdot b\cdot c \)
lemma (in group0) trans_neutral_image:

assumes \( V\subseteq G \)

shows \( \text{RightTranslation}(G,P,1 )(V) = V \) and \( \text{LeftTranslation}(G,P,1 )(V) = V \)
lemma (in topgroup) interval_add_zero:

assumes \( A\subseteq G \), \( 0 \in A \)

shows \( 0 \in A + A \)
corollary (in topgroup) elements_in_set_sum_inv:

assumes \( A\subseteq G \), \( B\subseteq G \), \( t=s + q \), \( s\in A \), \( q\in B \)

shows \( t \in A + B \)
lemma (in topgroup) roelcke_uniformity: shows \( \text{roelckeUniformity} \text{ is a uniformity on } G \)
lemma (in topgroup) interval_add:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( A + B \subseteq G \), \( A + B = f(A\times B) \), \( A + B = (\bigcup x\in A.\ x + B) \), \( A + B = \{x + y.\ \langle x,y\rangle \in A\times B\} \)
lemma (in topgroup) rtrans_interior:

assumes \( g\in G \) and \( A\subseteq G \)

shows \( int(A) + g = int(A + g) \)
lemma (in topgroup) interval_add:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( A + B \subseteq G \), \( A + B = f(A\times B) \), \( A + B = (\bigcup x\in A.\ x + B) \), \( A + B = \{x + y.\ \langle x,y\rangle \in A\times B\} \)
lemma (in topgroup) ltrans_interior:

assumes \( g\in G \) and \( A\subseteq G \)

shows \( g + int(A) = int(g + A) \)
lemma union_open:

assumes \( T \text{ is a topology } \) and \( \forall A\in \mathcal{A} .\ A \in T \)

shows \( (\bigcup \mathcal{A} ) \in T \)
lemma (in topgroup) elem_in_int_rtrans:

assumes \( g\in G \) and \( H \in \mathcal{N}_0 \)

shows \( g \in int(H + g) \) and \( g \in int(H + g) + int(H) \)
lemma (in topgroup) lrtrans_neigh:

assumes \( W\in \mathcal{N}_0 \) and \( x\in G \)

shows \( x + (W + ( - x)) \in \mathcal{N}_0 \) and \( (x + W) + ( - x) \in \mathcal{N}_0 \)
lemma (in topgroup) lrtrans_image:

assumes \( V\subseteq G \), \( x\in G \)

shows \( x + V = \{x + v.\ v\in V\} \), \( V + x = \{v + x.\ v\in V\} \)
lemma (in group0) lrtrans_in_group:

assumes \( x\in G \)

shows \( \text{LeftTranslation}(G,P,x)(V) \subseteq G \) and \( \text{RightTranslation}(G,P,x)(V) \subseteq G \)
lemma (in group0) cancel_middle:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( (a\cdot b)^{-1}\cdot (a\cdot c) = b^{-1}\cdot c \), \( (a\cdot b)\cdot (c\cdot b)^{-1} = a\cdot c^{-1} \), \( a^{-1}\cdot (a\cdot b\cdot c)\cdot c^{-1} = b \), \( a\cdot (b\cdot c^{-1})\cdot c = a\cdot b \)
corollary (in topgroup) elements_in_ltrans_inv:

assumes \( B\subseteq G \), \( g\in G \), \( q\in B \), \( t=g + q \)

shows \( t \in g + B \)
lemma (in topgroup) trans_subset:

assumes \( A \subseteq (( - x) + B) \), \( x\in G \), \( B\subseteq G \)

shows \( x + A \subseteq B \)
543
249
70
70