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.
Natural uniformities in topological groups: definitions 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
}
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
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
}
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
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 {
}
}
ultimately have \( id(G)\subseteq U \wedge (\exists Z\in \text{ leftUniformity }.\ Z\circ Z\subseteq U) \wedge converse(U)\in \text{ leftUniformity } \)
{
}
}
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
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 \)
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 {
}
}
ultimately have \( id(G)\subseteq U \wedge (\exists Z\in \text{ rightUniformity }.\ Z\circ Z\subseteq U) \wedge converse(U)\in \text{ rightUniformity } \)
{
}
}
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
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 \)
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 {
}
ultimately have \( ( - x) + t\in (( - x) + U) \longleftrightarrow t:U \)
assume t: \( t\in U \)
with \( U\subseteq G \), \( ( - x)\in G \) have \( ( - x) + t \in (( - x) + U) \) using lrtrans_image(1)
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 {
}
ultimately have \( t + ( - x)\in (U + ( - x)) \longleftrightarrow t:U \)
assume \( t\in U \)
with \( ( - x)\in G \), \( U\subseteq G \) have \( t + ( - x)\in (U + ( - x)) \) using lrtrans_image(2)
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 {
}
}
}
}
}
}
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 \)
qed
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
then show \( \text{UniformTopology}(\text{ leftUniformity },G) = T \) and \( \text{UniformTopology}(\text{ rightUniformity },G) = T \) using uniftop_def_alt
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
qed
have \( \forall V \in \text{ leftUniformity }.\ P^{-1}(V) \in \text{ leftUniformity } \)proof
ultimately show \( thesis \) using IsUniformlyCont_def
{
}
}
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
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
qed
have \( \forall V \in \text{ rightUniformity }.\ P^{-1}(V) \in \text{ rightUniformity } \)proof
ultimately show \( thesis \) using IsUniformlyCont_def
{
}
}
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
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
qed
have \( converse(U) \in \Phi \)proof
moreover {
}
}
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
qed
from V(3) have \( converse(U) \subseteq G\times G \) unfolding converse_def
ultimately show \( converse(U) \in \text{roelckeUniformity} \) unfolding roelckeUniformity_def
have \( \exists Z\in \Phi .\ Z\circ Z \subseteq U \)proof
ultimately show \( id(G)\subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi \)
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 {
}
qed
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 \)
moreover
qed
have \( \text{roelckeUniformity} \text{ is a filter on } (G \times G) \)proof
ultimately show \( thesis \) using IsUniformity_def
{
}
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 {
}
moreover {
}
moreover {
}
moreover {
}
ultimately show \( thesis \) unfolding IsFilter_def
qed
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 \)
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
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
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
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
qed
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 \)
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 {
}
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
ultimately have \( int(W + x) + (int(W)) = (\bigcup t\in int(W + x).\ int(t + W)) \)
{
}
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
with topSpaceAssum have \( int(W + x) + (int(W)) \in T \) using Top_2_L2, union_open
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 {
}
}
}
qed
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 \) using uniftop_def_alt
The inverse map is uniformly continuous in the Roelcke uniformity
theorem (in topgroup) inv_uniform_roelcke:
shows \( \text{GroupInv}(G,f) \text{ is uniformly continuous between } \text{roelckeUniformity}\text{ and } \text{roelckeUniformity} \)proof let \( P = \text{ProdFunction}( \text{GroupInv}(G,f), \text{GroupInv}(G,f)) \)
have L: \( \text{GroupInv}(G,f):G\rightarrow G \) and R: \( \text{roelckeUniformity} \text{ is a uniformity on } G \) using groupAssum, group0_2_T2, roelcke_uniformity
have \( \forall V \in \text{roelckeUniformity}.\ P^{-1}(V) \in \text{roelckeUniformity} \)proof
}
}
fix \( V \)
assume v: \( V\in \text{roelckeUniformity} \)
then obtain \( U \) where \( U \in \mathcal{N}_0 \) and \( \{\langle s,t\rangle \in G \times G .\ t \in U + s + U\} \subseteq V \) unfolding roelckeUniformity_def
with \( V \in \text{roelckeUniformity} \) have as: \( V \subseteq G \times G \), \( U \in \mathcal{N}_0 \), \( \{\langle s,t\rangle \in G \times G .\ t \in U + s + U\} \subseteq V \) unfolding roelckeUniformity_def
from as(2) obtain \( W \) where w: \( W \in \mathcal{N}_0 \), \( W \subseteq U \), \( (-W) = W \) using exists_sym_zerohood
from w(1) have wg: \( W\subseteq G \)
{
fix \( z \)
assume z: \( z \in \{\langle s,t\rangle \in G \times G .\ t \in W + s + W\} \)
then obtain \( s \) \( t \) where st: \( z=\langle s,t\rangle \), \( s\in G \), \( t\in G \)
from st(1), z have st2: \( t \in W + s + W \)
with \( W \in \mathcal{N}_0 \), st(2) obtain \( u \) \( v \) where uv: \( t=u + v \), \( u\in W + s \), \( v\in W \) using interval_add(4), lrtrans_in_group_add(2)
from \( W\subseteq G \), \( s\in G \), \( u\in W + s \) obtain \( q \) where q: \( q\in W \), \( u=q + s \) using elements_in_rtrans
from w(2), as(2), q, st(2) have \( u\in U + s \) using lrtrans_image(2)
with w(2), uv(1,3), as(2), st(2) have \( t\in U + s + U \) using interval_add(4), lrtrans_in_group_add(2)
with st have \( z \in \{\langle s,t\rangle \in G \times G .\ t \in U + s + U\} \)
then have sub: \( \{\langle s,t\rangle \in G \times G .\ t \in W + s + W\} \subseteq \{\langle s,t\rangle \in G \times G .\ t \in U + s + U\} \)
{
fix \( z \)
assume z: \( z \in \{\langle s,t\rangle \in G \times G .\ t \in W + s + W\} \)
then obtain \( s \) \( t \) where st: \( z=\langle s,t\rangle \), \( s\in G \), \( t\in G \)
from st(1), z have st2: \( t \in W + s + W \)
with \( W \in \mathcal{N}_0 \) obtain \( u \) \( v \) where uv: \( t=u + v \), \( u\in W + s \), \( v\in W \) using interval_add(4), lrtrans_in_group_add(2), st(2)
from \( W\subseteq G \), \( s\in G \), \( u\in W + s \) obtain \( q \) where q: \( q\in W \), \( u=q + s \) using elements_in_rtrans
from \( W\subseteq G \), \( q\in W \), \( v\in W \) have \( q\in G \), \( v\in G \)
with \( q\in G \), \( v\in G \), \( u=q + s \), st(2), uv(1), q(2) have \( t=q + (s + v) \) using group_op_closed_add, group_oper_assoc
with st(2), \( q\in G \), \( v\in G \) have minust: \( ( - t) = ( - v) + ( - s) + ( - q) \) using group_inv_of_two, group_op_closed, group_inv_of_two
from q(1), wg have \( ( - q)\in -W \) using ginv_image_add(2)
with w(3) have minusq: \( ( - q)\in W \)
from uv(3), wg have \( ( - v)\in -W \) using ginv_image_add(2)
with w(3) have minusv: \( ( - v)\in W \)
with st(2), wg have \( ( - v) + ( - s) \in W + ( - s) \) using lrtrans_image(2), inverse_in_group
with minust, minusq, st(2), wg have \( ( - t)\in (W + ( - s)) + W \) using interval_add(4), inverse_in_group, lrtrans_in_group_add(2)
moreover
from st, groupAssum have \( P(z) = \langle \text{GroupInv}(G,f)(s), \text{GroupInv}(G,f)(t)\rangle \) using prodFunctionApp, group0_2_T2
with st(2,3) have \( P(z) = \langle - s, - t\rangle \)
ultimately have \( P(z) \in \{\langle s,t\rangle \in G \times G .\ t \in W + s + W\} \) using st(2,3), inverse_in_group
with sub have \( P(z) \in \{\langle s,t\rangle \in G \times G .\ t \in U + s + U\} \)
with as(3) have \( P(z) \in V \)
with z, L have \( z \in P^{-1}(V) \) using prodFunction, func1_1_L5A, vimage_iff
with w(1) have \( \exists U\in \mathcal{N}_0.\ \{\langle s,t\rangle \in G \times G .\ t \in U + s + U\} \subseteq P^{-1}(V) \)
with L show \( P^{-1}(V) \in \text{roelckeUniformity} \) unfolding roelckeUniformity_def using prodFunction, func1_1_L6A
qed
with L, R show \( thesis \) using IsUniformlyCont_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) \) and \( b(x)\in Y \) 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) \) lemma uniftop_def_alt: shows \( \text{UniformTopology}(\Phi ,X) = \{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\rightarrow Y \Longrightarrow \Phi \text{ is a uniformity on } X \Longrightarrow \Gamma \text{ is a uniformity on } Y \Longrightarrow \)
\( 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 \), \( a\cdot b^{-1}\cdot (b\cdot c^{-1}) = a\cdot c^{-1} \) 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 \) theorem group0_2_T2:
assumes \( \text{IsAgroup}(G,f) \)
shows \( \text{GroupInv}(G,f) : G\rightarrow G \) theorem (in topgroup) exists_sym_zerohood:
assumes \( U\in \mathcal{N}_0 \)
shows \( \exists V\in \mathcal{N}_0.\ (V\subseteq U \wedge (-V)=V) \) lemma (in group0) group_inv_of_two:
assumes \( a\in G \) and \( b\in G \)
shows \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \) lemma (in topgroup) ginv_image_add:
assumes \( V\subseteq G \)
shows \( (-V)\subseteq G \) and \( (-V) = \{ - x.\ x \in V\} \) lemma (in group0) inverse_in_group:
assumes \( x\in G \)
shows \( x^{-1}\in G \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8