IsarMathLib

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

theory TopologicalGroup_Uniformity_ZF imports TopologicalGroup_ZF_1 UniformSpace_ZF
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 \in \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\} \), \( \{\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 \in \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\} \), \( \{\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 \( x1 \) \( x2 \) \( x3 \) where x: \( x1\in G \), \( x2\in G \), \( x3\in G \), \( ( - x1) + x2 \in W \), \( ( - x2) + x3 \in W \), \( x=\langle x1,x3\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 ( - x1) + x2,( - x2) + x3\rangle :W\times W \)
with WW have \( f(\langle ( - x1) + x2,( - x2) + x3\rangle ):f(W\times W) \) using func_imagedef , topgroup_f_binop
ultimately have \( (( - x1) + x2) + (( - x2) + x3) :W + W \)
moreover
from x(1,2,3) have \( (( - x1) + x2) + (( - x2) + x3) = ( - x1) + x3 \) using cancel_middle(2)
ultimately have \( ( - x1) + x3\in W + W \)
with W(2) have \( ( - x1) + x3\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 \( x1 \) \( x2 \) \( x3 \) where x: \( x1:G \), \( x2:G \), \( x3:G \), \( x1 + ( - x2) \in W \), \( x2 + ( - x3) \in W \), \( x=\langle x1,x3\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 x1 + ( - x2),x2 + ( - x3)\rangle \in W\times W \)
with WW have \( f(\langle x1 + ( - x2),x2 + ( - x3)\rangle ) \in f(W\times W) \) using func_imagedef , topgroup_f_binop
ultimately have \( (x1 + ( - x2)) + (x2 + ( - x3)) \in W + W \)
moreover
from x(1,2,3) have \( (x1 + ( - x2)) + (x2 + ( - x3)) = x1 + ( - x3) \) using cancel_middle(1)
ultimately have \( x1 + ( - x3) \in W + W \)
with W(2) have \( x1 + ( - x3) \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 ltrans_image_add
} 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 rtrans_image_add
} 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_trans
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 rtrans_image_add
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_trans_2
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 \) and \( \{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
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) = \{ - 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 \)
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:

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 \)
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:

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 \)
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) ltrans_image_add:

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

shows \( x + V = \{x + v.\ 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) rtrans_image_add:

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

shows \( 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_trans:

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

shows \( g \in int(g + 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_trans_2:

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

shows \( g \in int(H + g) \)
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)\} \)
284
108
36
36