IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory TopologicalGroup_ZF imports Topology_ZF_3 Group_ZF_1 Semigroup_ZF

begin

This theory is about the first subject of algebraic topology: topological groups.

Topological group: definition and notation

Topological group is a group that is a topological space at the same time. This means that a topological group is a triple of sets, say \((G,f,T)\) such that \(T\) is a topology on \(G\), \(f\) is a group operation on \(G\) and both \(f\) and the operation of taking inverse in \(G\) are continuous. Since IsarMathLib defines topology without using the carrier, (see Topology_ZF), in our setup we just use \(\bigcup T\) instead of \(G\) and say that the pair of sets \((\bigcup T , f)\) is a group. This way our definition of being a topological group is a statement about two sets: the topology \(T\) and the group operation \(f\) on \(G=\bigcup T\). Since the domain of the group operation is \(G\times G\), the pair of topologies in which \(f\) is supposed to be continuous is \(T\) and the product topology on \(G\times G\) (which we will call \(\tau\) below).

This way we arrive at the following definition of a predicate that states that pair of sets is a topological group.

definition

\( \text{IsAtopologicalGroup}(T,f) \equiv (T \text{ is a topology }) \wedge \text{IsAgroup}(\bigcup T,f) \wedge \) \( \text{IsContinuous}( \text{ProductTopology}(T,T),T,f) \wedge \) \( \text{IsContinuous}(T,T, \text{GroupInv}(\bigcup T,f)) \)

We will inherit notation from the topology0 locale. That locale assumes that \(T\) is a topology. For convenience we will denote \(G=\bigcup T\) and \(\tau\) to be the product topology on \(G\times G\). To that we add some notation specific to groups. We will use additive notation for the group operation, even though we don't assume that the group is abelian. The notation \(g+A\) will mean the left translation of the set \(A\) by element \(g\), i.e. \(g+A=\{g+a|a\in A\}\). The group operation \(G\) induces a natural operation on the subsets of \(G\) defined as \(\langle A,B\rangle \mapsto \{x+y | x\in A, y\in B \}\). Such operation has been considered in func_ZF and called \(f\) ''lifted to subsets of'' \(G\). We will denote the value of such operation on sets \(A,B\) as \(A+B\). The set of neigboorhoods of zero (denoted \( \mathcal{N}_0 \)) is the collection of (not necessarily open) sets whose interior contains the neutral element of the group.

locale topgroup = topology0 +

defines \( G \equiv \bigcup T \)

defines \( \tau \equiv \text{ProductTopology}(T,T) \)

assumes Ggroup: \( \text{IsAgroup}(G,f) \)

assumes fcon: \( \text{IsContinuous}(\tau ,T,f) \)

assumes inv_cont: \( \text{IsContinuous}(T,T, \text{GroupInv}(G,f)) \)

defines \( x + y \equiv f\langle x,y\rangle \)

defines \( ( - x) \equiv \text{GroupInv}(G,f)(x) \)

defines \( x - y \equiv x + ( - y) \)

defines \( -A \equiv \text{GroupInv}(G,f)(A) \)

defines \( x + A \equiv \text{LeftTranslation}(G,f,x)(A) \)

defines \( A + x \equiv \text{RightTranslation}(G,f,x)(A) \)

defines \( A + B \equiv (f \text{ lifted to subsets of } G)\langle A,B\rangle \)

defines \( 0 \equiv \text{ TheNeutralElement}(G,f) \)

defines \( \mathcal{N}_0 \equiv \{A \in Pow(G).\ 0 \in int(A)\} \)

defines \( \sum k \equiv \text{Fold1}(f,k) \)

The first lemma states that we indeeed talk about topological group in the context of topgroup locale.

lemma (in topgroup) topGroup:

shows \( \text{IsAtopologicalGroup}(T,f) \) using topSpaceAssum, Ggroup, fcon, inv_cont, IsAtopologicalGroup_def

If a pair of sets \((T,f)\) forms a topological group, then all theorems proven in the topgroup context are valid as applied to \((T,f)\).

lemma topGroupLocale:

assumes \( \text{IsAtopologicalGroup}(T,f) \)

shows \( topgroup(T,f) \) using assms, IsAtopologicalGroup_def, topgroup_def, topgroup_axioms.intro, topology0_def

We can use the group0 locale in the context of topgroup.

lemma (in topgroup) group0_valid_in_tgroup:

shows \( group0(G,f) \) using Ggroup, group0_def

We can use the group0 locale in the context of topgroup.

sublocale topgroup < group0

unfolding group0_def, gzero_def, grop_def, grinv_def using Ggroup

We can use semigr0 locale in the context of topgroup.

lemma (in topgroup) semigr0_valid_in_tgroup:

shows \( semigr0(G,f) \) using Ggroup, IsAgroup_def, IsAmonoid_def, semigr0_def

We can use the prod_top_spaces0 locale in the context of topgroup.

lemma (in topgroup) prod_top_spaces0_valid:

shows \( prod\_top\_spaces0(T,T,T) \) using topSpaceAssum, prod_top_spaces0_def

Negative of a group element is in group.

lemma (in topgroup) neg_in_tgroup:

assumes \( g\in G \)

shows \( ( - g) \in G \) using assms, inverse_in_group

Sum of two group elements is in the group.

lemma (in topgroup) group_op_closed_add:

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

shows \( x_1 + x_2 \in G \) using assms, group_op_closed

Zero is in the group.

lemma (in topgroup) zero_in_tgroup:

shows \( 0 \in G \) using group0_2_L2

Another lemma about canceling with two group elements written in additive notation

lemma (in topgroup) inv_cancel_two_add:

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

shows \( x_1 + ( - x_2) + x_2 = x_1 \), \( x_1 + x_2 + ( - x_2) = x_1 \), \( ( - x_1) + (x_1 + x_2) = x_2 \), \( x_1 + (( - x_1) + x_2) = x_2 \) using assms, inv_cancel_two

Useful identities proven in the Group_ZF theory, rewritten here in additive notation. Note since the group operation notation is left associative we don't really need the first set of parentheses in some cases.

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

from assms have \( x_1 + ( - x_3) = (x_1 + ( - x_2)) + (x_2 + ( - x_3)) \) using group0_2_L14A(1)

thus \( (x_1 + ( - x_2)) + (x_2 + ( - x_3)) = x_1 + ( - x_3) \)

from assms have \( ( - x_1) + x_3 = (( - x_1) + x_2) + (( - x_2) + x_3) \) using group0_2_L14A(2)

thus \( (( - x_1) + x_2) + (( - x_2) + x_3) = ( - x_1) + x_3 \)

from assms show \( ( - (x_1 + x_2)) + (x_1 + x_3) = ( - x_2) + x_3 \) using cancel_middle(1)

from assms show \( (x_1 + x_2) + ( - (x_3 + x_2)) =x_1 + ( - x_3) \) using cancel_middle(2)

from assms show \( ( - x_1) + (x_1 + x_2 + x_3) + ( - x_3) = x_2 \) using cancel_middle(3)

qed

We can cancel an element on the right from both sides of an equation.

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 \) using assms, cancel_right

We can cancel an element on the left from both sides of an equation.

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 \) using assms, cancel_left

We can put an element on the other side of an equation.

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 \) using assms, group0_2_L18

A simple equation from lemma simple_equation0 in Group_ZF in additive notation

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) \) using assms, simple_equation0

A simple equation from lemma simple_equation1 in Group_ZF in additive notation

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 \) using assms, simple_equation1

The set comprehension form of negative of a set. The proof uses the ginv_image lemma from Group_ZF theory which states the same thing in multiplicative notation.

lemma (in topgroup) ginv_image_add:

assumes \( V\subseteq G \)

shows \( (-V)\subseteq G \) and \( (-V) = \{ - x.\ x \in V\} \) using assms, ginv_image

The additive notation version of ginv_image_el lemma from Group_ZF theory

lemma (in topgroup) ginv_image_el_add:

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

shows \( ( - x) \in V \) using assms, ginv_image_el

Of course the product topology is a topology (on \(G\times G\)).

lemma (in topgroup) prod_top_on_G:

shows \( \tau \text{ is a topology } \) and \( \bigcup \tau = G\times G \) using topSpaceAssum, Top_1_4_T1

Let's recall that \(f\) is a binary operation on \(G\) in this context.

lemma (in topgroup) topgroup_f_binop:

shows \( f : G\times G \rightarrow G \) using Ggroup, group0_def, group_oper_fun

A subgroup of a topological group is a topological group with relative topology and restricted operation. Relative topology is the same as \( T \text{ restricted to } H \) which is defined to be \(\{V \cap H: V\in T\}\) in ZF1 theory.

lemma (in topgroup) top_subgroup:

assumes A1: \( \text{IsAsubgroup}(H,f) \)

shows \( \text{IsAtopologicalGroup}(T \text{ restricted to } H,\text{restrict}(f,H\times H)) \)proof

let \( \tau _0 = T \text{ restricted to } H \)

let \( f_H = \text{restrict}(f,H\times H) \)

have \( \bigcup \tau _0 = G \cap H \) using union_restrict

also

from A1 have \( \ldots = H \) using group0_3_L2

finally have \( \bigcup \tau _0 = H \)

have \( \tau _0 \text{ is a topology } \) using Top_1_L4

moreover

from A1, \( \bigcup \tau _0 = H \) have \( \text{IsAgroup}(\bigcup \tau _0,f_H) \) using IsAsubgroup_def

moreover

have \( \text{IsContinuous}( \text{ProductTopology}(\tau _0,\tau _0),\tau _0,f_H) \)proof

have \( two\_top\_spaces0(\tau , T,f) \) using topSpaceAssum, prod_top_on_G, topgroup_f_binop, prod_top_on_G, two_top_spaces0_def

moreover

from A1 have \( H \subseteq G \) using group0_3_L2

then have \( H\times H \subseteq \bigcup \tau \) using prod_top_on_G

moreover

have \( \text{IsContinuous}(\tau ,T,f) \) using fcon

ultimately have \( \text{IsContinuous}(\tau \text{ restricted to } H\times H, T \text{ restricted to } f_H(H\times H),f_H) \) using restr_restr_image_cont

moreover

have \( \text{ProductTopology}(\tau _0,\tau _0) = \tau \text{ restricted to } H\times H \) using topSpaceAssum, prod_top_restr_comm

moreover

from A1 have \( f_H(H\times H) = H \) using image_subgr_op

ultimately show \( thesis \)

qed

moreover

have \( \text{IsContinuous}(\tau _0,\tau _0, \text{GroupInv}(\bigcup \tau _0,f_H)) \)proof

let \( g = \text{restrict}( \text{GroupInv}(G,f),H) \)

have \( \text{GroupInv}(G,f) : G \rightarrow G \) using Ggroup, group0_2_T2

then have \( two\_top\_spaces0(T,T, \text{GroupInv}(G,f)) \) using topSpaceAssum, two_top_spaces0_def

moreover

from A1 have \( H \subseteq \bigcup T \) using group0_3_L2

ultimately have \( \text{IsContinuous}(\tau _0,T \text{ restricted to } g(H),g) \) using inv_cont, restr_restr_image_cont

moreover

from A1 have \( g(H) = H \) using restr_inv_onto

moreover

from A1 have \( \text{GroupInv}(H,f_H) = g \) using group0_3_T1

with \( \bigcup \tau _0 = H \) have \( g = \text{GroupInv}(\bigcup \tau _0,f_H) \)

ultimately show \( thesis \)

qed

ultimately show \( thesis \) unfolding IsAtopologicalGroup_def

qed

Interval arithmetic, translations and inverse of set

In this section we list some properties of operations of translating a set and reflecting it around the neutral element of the group. Many of the results are proven in other theories, here we just collect them and rewrite in notation specific to the topgroup context.

Different ways of looking at adding sets.

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\} \)proof

from assms show \( A + B \subseteq G \) and \( A + B = f(A\times B) \) and \( A + B = \{x + y.\ \langle x,y\rangle \in A\times B\} \) using topgroup_f_binop, lift_subsets_explained

from assms show \( A + B = (\bigcup x\in A.\ x + B) \) using image_ltrans_union

qed

If the neutral element is in a set, then it is in the sum of the sets.

lemma (in topgroup) interval_add_zero:

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

shows \( 0 \in A + A \)proof

from assms have \( 0 + 0 \in A + A \) using interval_add(4)

then show \( 0 \in A + A \) using group0_2_L2

qed

Some lemmas from Group_ZF_1 about images of set by translations written in additive notation

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\} \) using assms, ltrans_image, rtrans_image

Right and left translations of a set are subsets of the group. This is of course typically applied to the subsets of the group, but formally we don't need to assume that.

lemma (in topgroup) lrtrans_in_group_add:

assumes \( x\in G \)

shows \( x + V \subseteq G \) and \( V + x \subseteq G \) using assms, lrtrans_in_group

A corollary from interval_add

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 \) using assms, interval_add(4)

A corollary from lrtrans_image

corollary (in topgroup) elements_in_ltrans:

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

shows \( \exists q\in B.\ t=g + q \) using assms, lrtrans_image(1)

Another corollary of lrtrans_image

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 \) using assms, lrtrans_image(2)

Another corollary from interval_add

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 \) using assms, interval_add

Another corollary of lrtrans_image

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 \) using assms, lrtrans_image(1)

Another corollary of rtrans_image_add

lemma (in topgroup) elements_in_rtrans_inv:

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

shows \( t \in B + g \) using assms, lrtrans_image(2)

Right and left translations are continuous.

lemma (in topgroup) trans_cont:

assumes \( g\in G \)

shows \( \text{IsContinuous}(T,T, \text{RightTranslation}(G,f,g)) \) and \( \text{IsContinuous}(T,T, \text{LeftTranslation}(G,f,g)) \) using assms, trans_eq_section, topgroup_f_binop, fcon, prod_top_spaces0_valid, fix_1st_var_cont, fix_2nd_var_cont

Left and right translations of an open set are open.

lemma (in topgroup) open_tr_open:

assumes \( g\in G \) and \( V\in T \)

shows \( g + V \in T \) and \( V + g \in T \) using assms, neg_in_tgroup, trans_cont, IsContinuous_def, trans_image_vimage

Right and left translations are homeomorphisms.

lemma (in topgroup) tr_homeo:

assumes \( g\in G \)

shows \( \text{IsAhomeomorphism}(T,T, \text{RightTranslation}(G,f,g)) \) and \( \text{IsAhomeomorphism}(T,T, \text{LeftTranslation}(G,f,g)) \) using assms, trans_bij, trans_cont, open_tr_open, bij_cont_open_homeo

Left translations preserve interior.

lemma (in topgroup) ltrans_interior:

assumes A1: \( g\in G \) and A2: \( A\subseteq G \)

shows \( g + int(A) = int(g + A) \)proof

from assms have \( A \subseteq \bigcup T \) and \( \text{IsAhomeomorphism}(T,T, \text{LeftTranslation}(G,f,g)) \) using tr_homeo

then show \( thesis \) using int_top_invariant

qed

Right translations preserve interior.

lemma (in topgroup) rtrans_interior:

assumes A1: \( g\in G \) and A2: \( A\subseteq G \)

shows \( int(A) + g = int(A + g) \)proof

from assms have \( A \subseteq \bigcup T \) and \( \text{IsAhomeomorphism}(T,T, \text{RightTranslation}(G,f,g)) \) using tr_homeo

then show \( thesis \) using int_top_invariant

qed

Translating by an inverse and then by an element cancels out.

lemma (in topgroup) trans_inverse_elem:

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

shows \( g + (( - g) + A) = A \) using assms, neg_in_tgroup, trans_comp_image, group0_2_L6, trans_neutral, image_id_same

Inverse of an open set is open.

lemma (in topgroup) open_inv_open:

assumes \( V\in T \)

shows \( (-V) \in T \) using assms, inv_image_vimage, inv_cont, IsContinuous_def

Inverse is a homeomorphism.

lemma (in topgroup) inv_homeo:

shows \( \text{IsAhomeomorphism}(T,T, \text{GroupInv}(G,f)) \) using group_inv_bij, inv_cont, open_inv_open, bij_cont_open_homeo

Taking negative preserves interior.

lemma (in topgroup) int_inv_inv_int:

assumes \( A \subseteq G \)

shows \( int(-A) = -(int(A)) \) using assms, inv_homeo, int_top_invariant

Neighborhoods of zero

Zero neighborhoods are (not necessarily open) sets whose interior contains the neutral element of the group. In the topgroup locale the collection of neighboorhoods of zero is denoted \( \mathcal{N}_0 \).

The whole space is a neighborhood of zero.

lemma (in topgroup) zneigh_not_empty:

shows \( G \in \mathcal{N}_0 \) using topSpaceAssum, IsATopology_def, Top_2_L3, zero_in_tgroup

Any element that belongs to a subset of the group belongs to that subset with the interior of a neighborhood of zero added.

lemma (in topgroup) elem_in_int_sad:

assumes \( A\subseteq G \), \( g\in A \), \( H \in \mathcal{N}_0 \)

shows \( g \in A + int(H) \)proof

from assms(3) have \( 0 \in int(H) \) and \( int(H) \subseteq G \) using Top_2_L2

with assms(1,2) have \( g + 0 \in A + int(H) \) using elements_in_set_sum_inv

with assms(1,2) show \( thesis \) using group0_2_L2

qed

Any element belongs to the interior of any neighboorhood of zero left translated by that element.

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

from assms(2) have \( 0 \in int(H) \) and \( int(H) \subseteq G \) using Top_2_L2

with assms(1) have \( g \in g + int(H) \) using neut_trans_elem

with assms show \( g \in int(g + H) \) using ltrans_interior

from assms(1) have \( int(g + H) \subseteq G \) using lrtrans_in_group_add(1), Top_2_L1

with \( g \in int(g + H) \), assms(2) show \( g \in int(g + H) + int(H) \) using elem_in_int_sad

qed

Any element belongs to the interior of any neighboorhood of zero right translated by that element.

lemma (in topgroup) elem_in_int_rtrans:

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

shows \( g \in int(H + g) \) and \( g \in int(H + g) + int(H) \)proof

from A2 have \( 0 \in int(H) \) and \( int(H) \subseteq G \) using Top_2_L2

with A1 have \( g \in int(H) + g \) using neut_trans_elem

with assms show \( g \in int(H + g) \) using rtrans_interior

from assms(1) have \( int(H + g) \subseteq G \) using lrtrans_in_group_add(2), Top_2_L1

with \( g \in int(H + g) \), assms(2) show \( g \in int(H + g) + int(H) \) using elem_in_int_sad

qed

Negative of a neighborhood of zero is a neighborhood of zero.

lemma (in topgroup) neg_neigh_neigh:

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

shows \( (-H) \in \mathcal{N}_0 \)proof

from assms have \( int(H) \subseteq G \) and \( 0 \in int(H) \) using Top_2_L1

with assms have \( 0 \in int(-H) \) using neut_inv_neut, int_inv_inv_int

moreover

have \( \text{GroupInv}(G,f):G\rightarrow G \) using Ggroup, group0_2_T2

then have \( (-H) \subseteq G \) using func1_1_L6

ultimately show \( thesis \)

qed

Left translating an open set by a negative of a point that belongs to it makes it a neighboorhood of zero.

lemma (in topgroup) open_trans_neigh:

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

shows \( ( - g) + U \in \mathcal{N}_0 \)proof

let \( H = ( - g) + U \)

from assms have \( g\in G \)

then have \( ( - g) \in G \) using neg_in_tgroup

with A1 have \( H\in T \) using open_tr_open

hence \( H \subseteq G \)

moreover

have \( 0 \in int(H) \)proof

from assms have \( U\subseteq G \) and \( g\in U \)

with \( H\in T \) show \( 0 \in int(H) \) using elem_trans_neut, Top_2_L3

qed

ultimately show \( thesis \)

qed

Right translating an open set by a negative of a point that belongs to it makes it a neighboorhood of zero.

lemma (in topgroup) open_trans_neigh_2:

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

shows \( U + ( - g) \in \mathcal{N}_0 \)proof

let \( H = U + ( - g) \)

from assms have \( g\in G \)

then have \( ( - g) \in G \) using neg_in_tgroup

with A1 have \( H\in T \) using open_tr_open

hence \( H \subseteq G \)

moreover

have \( 0 \in int(H) \)proof

from assms have \( U\subseteq G \) and \( g\in U \)

with \( H\in T \) show \( 0 \in int(H) \) using elem_trans_neut, Top_2_L3

qed

ultimately show \( thesis \)

qed

Right and left translating an neighboorhood of zero by a point and its negative makes it back a neighboorhood of zero.

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

from assms(2) have \( x + (W + ( - x)) \subseteq G \) using lrtrans_in_group_add(1)

moreover

have \( 0 \in int(x + (W + ( - x))) \)proof

from assms(2) have \( int(W + ( - x)) \subseteq G \) using neg_in_tgroup, lrtrans_in_group_add(2), Top_2_L1

with assms(2) have \( (x + int((W + ( - x)))) = \{x + y.\ y\in int(W + ( - x))\} \) using lrtrans_image(1)

moreover

from assms have \( ( - x) \in int(W + ( - x)) \) using neg_in_tgroup, elem_in_int_rtrans(1)

ultimately have \( x + ( - x) \in x + int(W + ( - x)) \)

with assms show \( thesis \) using group0_2_L6, neg_in_tgroup, lrtrans_in_group_add(2), ltrans_interior

qed

ultimately show \( x + (W + ( - x)) \in \mathcal{N}_0 \)

from assms(2) have \( (x + W) + ( - x) \subseteq G \) using lrtrans_in_group_add(2), neg_in_tgroup

moreover

have \( 0 \in int((x + W) + ( - x)) \)proof

from assms(2) have \( int((x + W)) \subseteq G \) using lrtrans_in_group_add(1), Top_2_L1

with assms(2) have \( int(x + W) + ( - x) = \{y + ( - x).\ y\in int(x + W)\} \) using neg_in_tgroup, lrtrans_image(2)

moreover

from assms have \( x \in int(x + W) \) using elem_in_int_ltrans(1)

ultimately have \( x + ( - x) \in int(x + W) + ( - x) \)

with assms(2) have \( 0 \in int(x + W) + ( - x) \) using group0_2_L6

with assms show \( thesis \) using group0_2_L6, neg_in_tgroup, lrtrans_in_group_add(1), rtrans_interior

qed

ultimately show \( (x + W) + ( - x) \in \mathcal{N}_0 \)

qed

If \(A\) is a subset of \(B\) translated by \(-x\) then its translation by \(x\) is a subset of \(B\).

lemma (in topgroup) trans_subset:

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

shows \( x + A \subseteq B \)proof

from assms(1) have \( x + A \subseteq (x + (( - x) + B)) \)

with assms(2,3) show \( x + A \subseteq B \) using neg_in_tgroup, trans_comp_image, group0_2_L6, trans_neutral, image_id_same

qed

Every neighborhood of zero has a symmetric subset that is a neighborhood of zero.

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

let \( V = U\cap (-U) \)

have \( U\subseteq G \) using assms unfolding zerohoods_def

then have \( V\subseteq G \)

have invg: \( \text{GroupInv}(G, f) \in G \rightarrow G \) using group0_2_T2, Ggroup

have invb: \( \text{GroupInv}(G, f) \in \text{bij}(G,G) \) using group_inv_bij(2)

have \( (-V)= \text{GroupInv}(G,f)^{-1}V \) unfolding setninv_def using inv_image_vimage

also

have \( \ldots =( \text{GroupInv}(G,f)^{-1}U)\cap ( \text{GroupInv}(G,f)^{-1}(-U)) \) using invim_inter_inter_invim, invg

also

have \( \ldots =(-U)\cap ( \text{GroupInv}(G,f)^{-1}( \text{GroupInv}(G,f)U)) \) unfolding setninv_def using inv_image_vimage

also

from \( U\subseteq G \) have \( \ldots =(-U)\cap U \) using inj_vimage_image, invb unfolding bij_def

finally have \( (-V)=V \)

then show \( V \subseteq U \wedge (- V) = V \)

from assms have \( (-U)\in \mathcal{N}_0 \) using neg_neigh_neigh

with assms have \( 0 \in int(U)\cap int(-U) \) unfolding zerohoods_def

moreover

have \( int(U)\cap int(-U) = int(V) \) using int_inter_int

ultimately have \( 0 \in int(V) \) by (rule set_mem_eq )

with \( V\subseteq G \) show \( V\in \mathcal{N}_0 \) using zerohoods_def

qed

We can say even more than in exists_sym_zerohood: every neighborhood of zero \(U\) has a symmetric subset that is a neighborhood of zero and its set double is contained in \(U\).

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

have \( int(U)\in T \) using Top_2_L2

then have \( f^{-1}(int(U))\in \tau \) using fcon, IsContinuous_def

moreover

have fne: \( f \langle 0 , 0 \rangle = 0 \) using group0_2_L2

moreover

have \( 0 \in int(U) \) using assms unfolding zerohoods_def

then have \( f ^{-1} \{ 0 \}\subseteq f^{-1}(int(U)) \) using func1_1_L8, vimage_def

then have \( \text{GroupInv}(G,f)\subseteq f^{-1}(int(U)) \) using group0_2_T3

then have \( \langle 0 , 0 \rangle \in f^{-1}(int(U)) \) using fne, zero_in_tgroup unfolding GroupInv_def

ultimately obtain \( W \) \( V \) where wop: \( W\in T \) and vop: \( V\in T \) and cartsub: \( W\times V\subseteq f^{-1}(int(U)) \) and zerhood: \( \langle 0 , 0 \rangle \in W\times V \) using prod_top_point_neighb, topSpaceAssum unfolding prodtop_def

then have \( 0 \in W \) and \( 0 \in V \)

then have \( 0 \in W\cap V \)

have sub: \( W\cap V\subseteq G \) using wop, vop, G_def

have assoc: \( f\in G\times G\rightarrow G \) using group_oper_fun

{

fix \( t \) \( s \)

assume \( t\in W\cap V \) and \( s\in W\cap V \)

then have \( t\in W \) and \( s\in V \)

then have \( \langle t,s\rangle \in W\times V \)

then have \( \langle t,s\rangle \in f^{-1}(int(U)) \) using cartsub

then have \( f\langle t,s\rangle \in int(U) \) using func1_1_L15, assoc

}

hence \( \{f\langle t,s\rangle .\ \langle t,s\rangle \in (W\cap V)\times (W\cap V)\}\subseteq int(U) \)

then have \( (W\cap V) + (W\cap V)\subseteq int(U) \) unfolding setadd_def using lift_subsets_explained(4), assoc, sub

then have \( (W\cap V) + (W\cap V)\subseteq U \) using Top_2_L1

from topSpaceAssum have \( W\cap V\in T \) using vop, wop unfolding IsATopology_def

then have \( int(W\cap V)=W\cap V \) using Top_2_L3

with sub, \( 0 \in W\cap V \) have \( W\cap V\in \mathcal{N}_0 \) unfolding zerohoods_def

then obtain \( Q \) where \( Q\in \mathcal{N}_0 \) and \( Q\subseteq W\cap V \) and \( (-Q)=Q \) using exists_sym_zerohood

then have \( Q\times Q\subseteq (W\cap V)\times (W\cap V) \)

moreover

from \( Q\subseteq W\cap V \) have \( W\cap V\subseteq G \) and \( Q\subseteq G \) using vop, wop unfolding G_def

ultimately have \( Q + Q\subseteq (W\cap V) + (W\cap V) \) using interval_add(2), func1_1_L8

with \( (W\cap V) + (W\cap V)\subseteq U \) have \( Q + Q\subseteq U \)

from \( Q\in \mathcal{N}_0 \) have \( 0 \in Q \) unfolding zerohoods_def using Top_2_L1

with \( Q + Q\subseteq U \), \( Q\subseteq G \) have \( 0 + Q\subseteq U \) using interval_add(3)

with \( Q\subseteq G \) have \( Q\subseteq U \) unfolding ltrans_def, gzero_def using trans_neutral(2), image_id_same

with \( Q\in \mathcal{N}_0 \), \( Q + Q\subseteq U \), \( (-Q)=Q \) show \( thesis \)

qed

Closure in topological groups

This section is devoted to a characterization of closure in topological groups.

Closure of a set is contained in the sum of the set and any neighboorhood of zero.

lemma (in topgroup) cl_contains_zneigh:

assumes A1: \( A\subseteq G \) and A2: \( H \in \mathcal{N}_0 \)

shows \( cl(A) \subseteq A + H \)proof

fix \( x \)

assume \( x \in cl(A) \)

from A1 have \( cl(A) \subseteq G \) using Top_3_L11

with \( x \in cl(A) \) have \( x\in G \)

have \( int(H) \subseteq G \) using Top_2_L2

let \( V = int(x + (-H)) \)

have \( V = x + (-int(H)) \)proof

from A2, \( x\in G \) have \( V = x + int(-H) \) using neg_neigh_neigh, ltrans_interior

with A2 show \( thesis \) using int_inv_inv_int

qed

have \( A\cap V \neq 0 \)proof

from A2, \( x\in G \), \( x \in cl(A) \) have \( V\in T \) and \( x \in cl(A) \cap V \) using neg_neigh_neigh, elem_in_int_ltrans(1), Top_2_L2

with A1 show \( A\cap V \neq 0 \) using cl_inter_neigh

qed

then obtain \( y \) where \( y\in A \) and \( y\in V \)

with \( V = x + (-int(H)) \), \( int(H) \subseteq G \), \( x\in G \) have \( x \in y + int(H) \) using ltrans_inv_in

with \( y\in A \) have \( x \in (\bigcup y\in A.\ y + H) \) using Top_2_L1, func1_1_L8

with assms show \( x \in A + H \) using interval_add(3)

qed

The next theorem provides a characterization of closure in topological groups in terms of neighborhoods of zero.

theorem (in topgroup) cl_topgroup:

assumes \( A\subseteq G \)

shows \( cl(A) = (\bigcap H\in \mathcal{N}_0.\ A + H) \)proof

from assms show \( cl(A) \subseteq (\bigcap H\in \mathcal{N}_0.\ A + H) \) using zneigh_not_empty, cl_contains_zneigh

next

{

fix \( x \)

assume \( x \in (\bigcap H\in \mathcal{N}_0.\ A + H) \)

then have \( x \in A + G \) using zneigh_not_empty

with assms have \( x\in G \) using interval_add

have \( \forall U\in T.\ x\in U \longrightarrow U\cap A \neq 0 \)proof

{

fix \( U \)

assume \( U\in T \) and \( x\in U \)

let \( H = -(( - x) + U) \)

from \( U\in T \), and, \( x\in U \) have \( ( - x) + U \subseteq G \) and \( H \in \mathcal{N}_0 \) using open_trans_neigh, neg_neigh_neigh

with \( x \in (\bigcap H\in \mathcal{N}_0.\ A + H) \) have \( x \in A + H \)

with assms, \( H \in \mathcal{N}_0 \) obtain \( y \) where \( y\in A \) and \( x \in y + H \) using interval_add(3)

have \( y\in U \)proof

from assms, \( y\in A \) have \( y\in G \)

with \( ( - x) + U \subseteq G \), and, \( x \in y + H \) have \( y \in x + (( - x) + U) \) using ltrans_inv_in

with \( U\in T \), \( x\in G \) show \( y\in U \) using neg_in_tgroup, trans_comp_image, group0_2_L6, trans_neutral, image_id_same

qed

with \( y\in A \) have \( U\cap A \neq 0 \)

}

thus \( thesis \)

qed

with assms, \( x\in G \) have \( x \in cl(A) \) using inter_neigh_cl

}

thus \( (\bigcap H\in \mathcal{N}_0.\ A + H) \subseteq cl(A) \)

qed

Sums of sequences of elements and subsets

In this section we consider properties of the function \(G^n\rightarrow G\), \(x=(x_0,x_1,...,x_{n-1})\mapsto \sum_{i=0}^{n-1}x_i\). We will model the cartesian product \(G^n\) by the space of sequences \(n\rightarrow G\), where \(n=\{0,1,...,n-1 \}\) is a natural number. This space is equipped with a natural product topology defined in Topology_ZF_3.

Let's recall first that the sum of elements of a group is an element of the group.

lemma (in topgroup) sum_list_in_group:

assumes \( n \in nat \) and \( x: succ(n)\rightarrow G \)

shows \( (\sum x) \in G \)proof

from assms have \( semigr0(G,f) \) and \( n \in nat \), \( x: succ(n)\rightarrow G \) using semigr0_valid_in_tgroup

then have \( \text{Fold1}(f,x) \in G \) by (rule prod_type )

thus \( (\sum x) \in G \)

qed

In this context \( x + y \) is the same as the value of the group operation on the elements \(x\) and \(y\). Normally we shouldn't need to state this a s separate lemma.

lemma (in topgroup) grop_def1:

shows \( f\langle x,y\rangle = x + y \)

Another theorem from Semigroup_ZF theory that is useful to have in the additive notation.

lemma (in topgroup) shorter_set_add:

assumes \( n \in nat \) and \( x: succ(succ(n))\rightarrow G \)

shows \( (\sum x) = (\sum \text{Init}(x)) + (x(succ(n))) \)proof

from assms have \( semigr0(G,f) \) and \( n \in nat \), \( x: succ(succ(n))\rightarrow G \) using semigr0_valid_in_tgroup

then have \( \text{Fold1}(f,x) = f\langle \text{Fold1}(f, \text{Init}(x)),x(succ(n))\rangle \) by (rule shorter_seq )

thus \( thesis \)

qed

Sum is a continuous function in the product topology.

theorem (in topgroup) sum_continuous:

assumes \( n \in nat \)

shows \( \text{IsContinuous}( \text{SeqProductTopology}(succ(n),T),T,\{\langle x,\sum x\rangle .\ x\in succ(n)\rightarrow G\}) \)proof

note \( n \in nat \)

moreover

have \( \text{IsContinuous}( \text{SeqProductTopology}(succ(0),T),T,\{\langle x,\sum x\rangle .\ x\in succ(0)\rightarrow G\}) \)proof

have \( \{\langle x,\sum x\rangle .\ x\in succ(0)\rightarrow G\} = \{\langle x,x(0)\rangle .\ x\in 1\rightarrow G\} \) using semigr0_valid_in_tgroup, prod_of_1elem

moreover

have \( \text{IsAhomeomorphism}( \text{SeqProductTopology}(1,T),T,\{\langle x,x(0)\rangle .\ x\in 1\rightarrow \bigcup T\}) \) using topSpaceAssum, singleton_prod_top1

ultimately show \( thesis \) using IsAhomeomorphism_def

qed

moreover

have \( \forall k\in nat.\ \) \( \text{IsContinuous}( \text{SeqProductTopology}(succ(k),T),T,\{\langle x,\sum x\rangle .\ x\in succ(k)\rightarrow G\})\) \( \longrightarrow \) \( \text{IsContinuous}( \text{SeqProductTopology}(succ(succ(k)),T),T,\{\langle x,\sum x\rangle .\ x\in succ(succ(k))\rightarrow G\}) \)proof

{

fix \( k \)

assume \( k \in nat \)

let \( s = \{\langle x,\sum x\rangle .\ x\in succ(k)\rightarrow G\} \)

let \( g = \{\langle p,\langle s(\text{fst}(p)),\text{snd}(p)\rangle \rangle .\ p \in (succ(k)\rightarrow G)\times G\} \)

let \( h = \{\langle x,\langle \text{Init}(x),x(succ(k))\rangle \rangle .\ x \in succ(succ(k))\rightarrow G\} \)

let \( \phi = \text{SeqProductTopology}(succ(k),T) \)

let \( \psi = \text{SeqProductTopology}(succ(succ(k)),T) \)

assume \( \text{IsContinuous}(\phi ,T,s) \)

from \( k \in nat \) have \( s: (succ(k)\rightarrow G) \rightarrow G \) using sum_list_in_group, ZF_fun_from_total

have \( h: (succ(succ(k))\rightarrow G)\rightarrow (succ(k)\rightarrow G)\times G \)proof

{

fix \( x \)

assume \( x \in succ(succ(k))\rightarrow G \)

with \( k \in nat \) have \( \text{Init}(x) \in (succ(k)\rightarrow G) \) using init_props

with \( k \in nat \), \( x : succ(succ(k))\rightarrow G \) have \( \langle \text{Init}(x),x(succ(k))\rangle \in (succ(k)\rightarrow G)\times G \) using apply_funtype

}

then show \( thesis \) using ZF_fun_from_total

qed

moreover

have \( g:((succ(k)\rightarrow G)\times G)\rightarrow (G\times G) \)proof

{

fix \( p \)

assume \( p \in (succ(k)\rightarrow G)\times G \)

hence \( \text{fst}(p): succ(k)\rightarrow G \) and \( \text{snd}(p) \in G \)

with \( s: (succ(k)\rightarrow G) \rightarrow G \) have \( \langle s(\text{fst}(p)),\text{snd}(p)\rangle \in G\times G \) using apply_funtype

}

then show \( g:((succ(k)\rightarrow G)\times G)\rightarrow (G\times G) \) using ZF_fun_from_total

qed

moreover

have \( f : G\times G \rightarrow G \) using topgroup_f_binop

ultimately have \( f\circ g\circ h :(succ(succ(k))\rightarrow G)\rightarrow G \) using comp_fun

from \( k \in nat \) have \( \text{IsContinuous}(\psi , \text{ProductTopology}(\phi ,T),h) \) using topSpaceAssum, finite_top_prod_homeo, IsAhomeomorphism_def

moreover

have \( \text{IsContinuous}( \text{ProductTopology}(\phi ,T),\tau ,g) \)proof

from topSpaceAssum have \( T \text{ is a topology } \), \( \phi \text{ is a topology } \), \( \bigcup \phi = succ(k)\rightarrow G \) using seq_prod_top_is_top

moreover

from \( \bigcup \phi = succ(k)\rightarrow G \), \( s: (succ(k)\rightarrow G) \rightarrow G \) have \( s:\bigcup \phi \rightarrow \bigcup T \)

moreover

note \( \text{IsContinuous}(\phi ,T,s) \)

moreover

from \( \bigcup \phi = succ(k)\rightarrow G \) have \( g = \{\langle p,\langle s(\text{fst}(p)),\text{snd}(p)\rangle \rangle .\ p \in \bigcup \phi \times \bigcup T\} \)

ultimately have \( \text{IsContinuous}( \text{ProductTopology}(\phi ,T), \text{ProductTopology}(T,T),g) \) using cart_prod_cont1

thus \( thesis \)

qed

moreover

have \( \text{IsContinuous}(\tau ,T,f) \) using fcon

moreover

have \( \{\langle x,\sum x\rangle .\ x\in succ(succ(k))\rightarrow G\} = f\circ g\circ h \)proof

let \( d = \{\langle x,\sum x\rangle .\ x\in succ(succ(k))\rightarrow G\} \)

from \( k\in nat \) have \( \forall x\in succ(succ(k))\rightarrow G.\ (\sum x) \in G \) using sum_list_in_group

then have \( d:(succ(succ(k))\rightarrow G)\rightarrow G \) using sum_list_in_group, ZF_fun_from_total

moreover

note \( f\circ g\circ h :(succ(succ(k))\rightarrow G)\rightarrow G \)

moreover

have \( \forall x\in succ(succ(k))\rightarrow G.\ d(x) = (f\circ g\circ h)(x) \)proof

fix \( x \)

assume \( x\in succ(succ(k))\rightarrow G \)

then have I: \( h(x) = \langle \text{Init}(x),x(succ(k))\rangle \) using ZF_fun_from_tot_val1

moreover

from \( k\in nat \), \( x\in succ(succ(k))\rightarrow G \) have \( \text{Init}(x): succ(k)\rightarrow G \) using init_props

moreover

from \( k\in nat \), \( x:succ(succ(k))\rightarrow G \) have II: \( x(succ(k)) \in G \) using apply_funtype

ultimately have \( h(x) \in (succ(k)\rightarrow G)\times G \)

then have \( g(h(x)) = \langle s(\text{fst}(h(x))),\text{snd}(h(x))\rangle \) using ZF_fun_from_tot_val1

with I have \( g(h(x)) = \langle s( \text{Init}(x)),x(succ(k))\rangle \)

with \( \text{Init}(x): succ(k)\rightarrow G \) have \( g(h(x)) = \langle \sum \text{Init}(x),x(succ(k))\rangle \) using ZF_fun_from_tot_val1

with \( k \in nat \), \( x: succ(succ(k))\rightarrow G \) have \( f(g(h(x))) = (\sum x) \) using shorter_set_add

with \( x \in succ(succ(k))\rightarrow G \) have \( f(g(h(x))) = d(x) \) using ZF_fun_from_tot_val1

moreover

from \( h: (succ(succ(k))\rightarrow G)\rightarrow (succ(k)\rightarrow G)\times G \), \( g:((succ(k)\rightarrow G)\times G)\rightarrow (G\times G) \), \( f:(G\times G)\rightarrow G \), \( x\in succ(succ(k))\rightarrow G \) have \( (f\circ g\circ h)(x) = f(g(h(x))) \) by (rule func1_1_L18 )

ultimately show \( d(x) = (f\circ g\circ h)(x) \)

qed

ultimately show \( \{\langle x,\sum x\rangle .\ x\in succ(succ(k))\rightarrow G\} = f\circ g\circ h \) using func_eq

qed

moreover

note \( \text{IsContinuous}(\tau ,T,f) \)

ultimately have \( \text{IsContinuous}(\psi ,T,\{\langle x,\sum x\rangle .\ x\in succ(succ(k))\rightarrow G\}) \) using comp_cont3

}

thus \( thesis \)

qed

ultimately show \( thesis \) by (rule ind_on_nat )

qed

end

Definition of IsAtopologicalGroup: \( \text{IsAtopologicalGroup}(T,f) \equiv (T \text{ is a topology }) \wedge \text{IsAgroup}(\bigcup T,f) \wedge \) \( \text{IsContinuous}( \text{ProductTopology}(T,T),T,f) \wedge \) \( \text{IsContinuous}(T,T, \text{GroupInv}(\bigcup T,f)) \)

Definition of IsAgroup: \( \text{IsAgroup}(G,f) \equiv \) \( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)

Definition of IsAmonoid: \( \text{IsAmonoid}(G,f) \equiv \) \( f \text{ is associative on } G \wedge \) \( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)

lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)

lemma (in group0) group_op_closed:

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

shows \( a\cdot b \in G \)

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 group0) inv_cancel_two:

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

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)

lemma (in group0) group0_2_L14A:

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

shows \( a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \), \( a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1} \), \( a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1} \), \( (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1} \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a \), \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b \)

lemma (in group0) group0_2_L14A:

assumes \( a\in G \), \( b\in G \), \( c\in 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} \)

lemma (in group0) cancel_middle:

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

lemma (in group0) cancel_middle:

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

lemma (in group0) cancel_right:

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

shows \( a = c \)

lemma (in group0) cancel_left:

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

shows \( b=c \)

lemma (in group0) group0_2_L18:

assumes \( a\in G \), \( b\in G \) and \( c = a\cdot b \)

shows \( c\cdot b^{-1} = a \), \( a^{-1}\cdot c = b \)

lemma (in group0) simple_equation0:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( a\cdot b^{-1} = c^{-1} \)

shows \( c = b\cdot a^{-1} \)

lemma (in group0) simple_equation1:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( a^{-1}\cdot b = c^{-1} \)

shows \( c = b^{-1}\cdot a \)

lemma (in group0) ginv_image:

assumes \( V\subseteq G \)

shows \( \text{GroupInv}(G,P)(V) \subseteq G \) and \( \text{GroupInv}(G,P)(V) = \{g^{-1}.\ g \in V\} \)

lemma (in group0) ginv_image_el:

assumes \( V\subseteq G \), \( g \in \text{GroupInv}(G,P)(V) \)

shows \( g^{-1} \in V \)

theorem Top_1_4_T1:

assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)

shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \)

lemma (in group0) group_oper_fun: shows \( P : G\times G\rightarrow G \)

lemma union_restrict: shows \( \bigcup (M \text{ restricted to } X) = (\bigcup M) \cap X \)

lemma (in group0) group0_3_L2:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( H \subseteq G \)

lemma (in topology0) Top_1_L4: shows \( (T \text{ restricted to } X) \text{ is a topology } \)

Definition of IsAsubgroup: \( \text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H, \text{restrict}(P,H\times H)) \)

lemma (in topgroup) prod_top_on_G: shows \( \tau \text{ is a topology } \) and \( \bigcup \tau = G\times G \)

lemma (in topgroup) topgroup_f_binop: shows \( f : G\times G \rightarrow G \)

lemma (in two_top_spaces0) restr_restr_image_cont:

assumes \( A \subseteq X_1 \) and \( f \text{ is continuous } \) and \( g = \text{restrict}(f,A) \) and \( \tau _3 = \tau _1 \text{ restricted to } A \)

shows \( \text{IsContinuous}(\tau _3, \tau _2 \text{ restricted to } g(A),g) \)

lemma prod_top_restr_comm:

assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)

shows \( \text{ProductTopology}(T \text{ restricted to } A,S \text{ restricted to } B) =\) \( \text{ProductTopology}(T,S) \text{ restricted to } (A\times B) \)

lemma image_subgr_op:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( \text{restrict}(P,H\times H)(H\times H) = H \)

theorem group0_2_T2:

assumes \( \text{IsAgroup}(G,f) \)

shows \( \text{GroupInv}(G,f) : G\rightarrow G \)

lemma (in group0) restr_inv_onto:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( \text{restrict}( \text{GroupInv}(G,P),H)(H) = H \)

theorem (in group0) group0_3_T1:

assumes \( \text{IsAsubgroup}(H,P) \) and \( g = \text{restrict}(P,H\times H) \)

shows \( \text{GroupInv}(H,g) = \text{restrict}( \text{GroupInv}(G,P),H) \)

lemma lift_subsets_explained:

assumes \( f : X\times X \rightarrow Y \) and \( A \subseteq X \), \( B \subseteq X \) and \( F = f \text{ lifted to subsets of } X \)

shows \( F\langle A,B\rangle \subseteq Y \) and \( F\langle A,B\rangle = f(A\times B) \), \( F\langle A,B\rangle = \{f(p).\ p \in A\times B\} \), \( F\langle A,B\rangle = \{f\langle x,y\rangle .\ \langle x,y\rangle \in A\times B\} \)

lemma (in group0) image_ltrans_union:

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

shows \( (P \text{ lifted to subsets of } G)\langle A,B\rangle = (\bigcup a\in A.\ \text{LeftTranslation}(G,P,a)(B)) \)

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 group0) ltrans_image:

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

shows \( \text{LeftTranslation}(G,P,x)(V) = \{x\cdot v.\ v\in V\} \)

lemma (in group0) rtrans_image:

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

shows \( \text{RightTranslation}(G,P,x)(V) = \{v\cdot 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 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) 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) 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 group0) trans_eq_section:

assumes \( g\in G \)

shows \( \text{RightTranslation}(G,P,g) = \text{Fix2ndVar}(P,g) \) and \( \text{LeftTranslation}(G,P,g) = \text{Fix1stVar}(P,g) \)

lemma (in topgroup) prod_top_spaces0_valid: shows \( prod\_top\_spaces0(T,T,T) \)

lemma (in prod_top_spaces0) fix_1st_var_cont:

assumes \( f: X_1\times X_2\rightarrow X_3 \) and \( \text{IsContinuous}(\eta ,\tau _3,f) \) and \( x\in X_1 \)

shows \( \text{IsContinuous}(\tau _2,\tau _3, \text{Fix1stVar}(f,x)) \)

lemma (in prod_top_spaces0) fix_2nd_var_cont:

assumes \( f: X_1\times X_2\rightarrow X_3 \) and \( \text{IsContinuous}(\eta ,\tau _3,f) \) and \( y\in X_2 \)

shows \( \text{IsContinuous}(\tau _1,\tau _3, \text{Fix2ndVar}(f,y)) \)

lemma (in topgroup) neg_in_tgroup:

assumes \( g\in G \)

shows \( ( - g) \in G \)

lemma (in topgroup) trans_cont:

assumes \( g\in G \)

shows \( \text{IsContinuous}(T,T, \text{RightTranslation}(G,f,g)) \) and \( \text{IsContinuous}(T,T, \text{LeftTranslation}(G,f,g)) \)

Definition of IsContinuous: \( \text{IsContinuous}(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)

lemma (in group0) trans_image_vimage:

assumes \( g\in G \)

shows \( \text{LeftTranslation}(G,P,g)(A) = \text{LeftTranslation}(G,P,g^{-1})^{-1}(A) \) and \( \text{RightTranslation}(G,P,g)(A) = \text{RightTranslation}(G,P,g^{-1})^{-1}(A) \)

lemma (in group0) trans_bij:

assumes \( g\in G \)

shows \( \text{RightTranslation}(G,P,g) \in \text{bij}(G,G) \) and \( \text{LeftTranslation}(G,P,g) \in \text{bij}(G,G) \)

lemma (in topgroup) open_tr_open:

assumes \( g\in G \) and \( V\in T \)

shows \( g + V \in T \) and \( V + g \in T \)

lemma bij_cont_open_homeo:

assumes \( f \in \text{bij}(\bigcup T,\bigcup S) \) and \( \text{IsContinuous}(T,S,f) \) and \( \forall U\in T.\ f(U) \in S \)

shows \( \text{IsAhomeomorphism}(T,S,f) \)

lemma (in topgroup) tr_homeo:

assumes \( g\in G \)

shows \( \text{IsAhomeomorphism}(T,T, \text{RightTranslation}(G,f,g)) \) and \( \text{IsAhomeomorphism}(T,T, \text{LeftTranslation}(G,f,g)) \)

theorem int_top_invariant:

assumes \( A\subseteq \bigcup T \) and \( \text{IsAhomeomorphism}(T,S,f) \)

shows \( f( \text{Interior}(A,T)) = \text{Interior}(f(A),S) \)

lemma (in group0) trans_comp_image:

assumes \( g\in G \), \( h\in G \) and \( T_g = \text{LeftTranslation}(G,P,g) \), \( T_h = \text{LeftTranslation}(G,P,h) \)

shows \( T_g(T_h(A)) = \text{LeftTranslation}(G,P,g\cdot h)(A) \)

lemma (in group0) group0_2_L6:

assumes \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)

lemma (in group0) trans_neutral: shows \( \text{RightTranslation}(G,P,1 ) = id(G) \) and \( \text{LeftTranslation}(G,P,1 ) = id(G) \)

lemma image_id_same:

assumes \( A\subseteq X \)

shows \( id(X)(A) = A \)

lemma (in group0) inv_image_vimage: shows \( \text{GroupInv}(G,P)(V) = \text{GroupInv}(G,P)^{-1}(V) \)

lemma (in group0) group_inv_bij: shows \( \text{GroupInv}(G,P)\circ \text{GroupInv}(G,P) = id(G) \) and \( \text{GroupInv}(G,P) \in \text{bij}(G,G) \) and \( \text{GroupInv}(G,P) = converse( \text{GroupInv}(G,P)) \)

lemma (in topgroup) open_inv_open:

assumes \( V\in T \)

shows \( (-V) \in T \)

lemma (in topgroup) inv_homeo: shows \( \text{IsAhomeomorphism}(T,T, \text{GroupInv}(G,f)) \)

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_L3: shows \( U\in T \longleftrightarrow int(U) = U \)

lemma (in topgroup) zero_in_tgroup: shows \( 0 \in G \)

lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)

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 group0) neut_trans_elem:

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

shows \( g \in \text{LeftTranslation}(G,P,g)(A) \), \( g \in \text{RightTranslation}(G,P,g)(A) \)

lemma (in topgroup) ltrans_interior:

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

shows \( g + int(A) = int(g + A) \)

lemma (in topgroup) lrtrans_in_group_add:

assumes \( x\in G \)

shows \( x + V \subseteq G \) and \( V + x \subseteq G \)

lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)

lemma (in topgroup) elem_in_int_sad:

assumes \( A\subseteq G \), \( g\in A \), \( H \in \mathcal{N}_0 \)

shows \( g \in A + int(H) \)

lemma (in topgroup) rtrans_interior:

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

shows \( int(A) + g = int(A + g) \)

lemma (in topgroup) lrtrans_in_group_add:

assumes \( x\in G \)

shows \( x + V \subseteq G \) and \( V + x \subseteq G \)

lemma (in group0) neut_inv_neut:

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

shows \( 1 \in \text{GroupInv}(G,P)(A) \)

lemma (in topgroup) int_inv_inv_int:

assumes \( A \subseteq G \)

shows \( int(-A) = -(int(A)) \)

lemma func1_1_L6:

assumes \( f:X\rightarrow Y \)

shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \)

lemma (in group0) elem_trans_neut:

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

shows \( 1 \in \text{LeftTranslation}(G,P,g^{-1})(A) \), \( 1 \in \text{RightTranslation}(G,P,g^{-1})(A) \)

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

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A\cap B) = f^{-1}(A) \cap f^{-1}(B) \)

lemma inj_vimage_image:

assumes \( f \in \text{inj}(X,Y) \) and \( A\subseteq X \)

shows \( f^{-1}(f(A)) = A \)

lemma (in topgroup) neg_neigh_neigh:

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

shows \( (-H) \in \mathcal{N}_0 \)

lemma (in topology0) int_inter_int: shows \( int(A) \cap int(B) = int(A\cap B) \)

lemma set_mem_eq:

assumes \( x\in A \), \( A=B \)

shows \( x\in B \)

lemma func1_1_L8:

assumes \( A\subseteq B \)

shows \( f(A)\subseteq f(B) \)

theorem (in group0) group0_2_T3: shows \( P^{-1}\{1 \} = \text{GroupInv}(G,P) \)

Definition of GroupInv: \( \text{GroupInv}(G,f) \equiv \{\langle x,y\rangle \in G\times G.\ f\langle x,y\rangle = \text{ TheNeutralElement}(G,f)\} \)

lemma prod_top_point_neighb:

assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( U \in \text{ProductTopology}(T,S) \) and \( x \in U \)

shows \( \exists V W.\ V\in T \wedge W\in S \wedge V\times W \subseteq U \wedge x \in V\times W \)

lemma func1_1_L15:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \)

lemma lift_subsets_explained:

assumes \( f : X\times X \rightarrow Y \) and \( A \subseteq X \), \( B \subseteq X \) and \( F = f \text{ lifted to subsets of } X \)

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 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) 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 group0) trans_neutral: shows \( \text{RightTranslation}(G,P,1 ) = id(G) \) and \( \text{LeftTranslation}(G,P,1 ) = id(G) \)

lemma (in topology0) Top_3_L11:

assumes \( A \subseteq \bigcup T \)

shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T - A) = \bigcup T - int(A) \)

lemma (in topology0) cl_inter_neigh:

assumes \( A \subseteq \bigcup T \) and \( U\in T \) and \( x \in cl(A) \cap U \)

shows \( A\cap U \neq 0 \)

lemma (in group0) ltrans_inv_in:

assumes \( V\subseteq G \) and \( y\in G \) and \( x \in \text{LeftTranslation}(G,P,y)( \text{GroupInv}(G,P)(V)) \)

shows \( y \in \text{LeftTranslation}(G,P,x)(V) \)

lemma (in topgroup) zneigh_not_empty: shows \( G \in \mathcal{N}_0 \)

lemma (in topgroup) cl_contains_zneigh:

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

shows \( cl(A) \subseteq A + H \)

lemma (in topgroup) open_trans_neigh:

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

shows \( ( - g) + U \in \mathcal{N}_0 \)

lemma (in topology0) inter_neigh_cl:

assumes \( A \subseteq \bigcup T \) and \( x\in \bigcup T \) and \( \forall U\in T.\ x\in U \longrightarrow U\cap A \neq 0 \)

shows \( x \in cl(A) \)

lemma (in topgroup) semigr0_valid_in_tgroup: shows \( semigr0(G,f) \)

lemma (in semigr0) prod_type:

assumes \( n \in nat \) and \( a : succ(n) \rightarrow G \)

shows \( (\prod a) \in G \)

lemma (in semigr0) shorter_seq:

assumes \( k \in nat \) and \( a \in succ(succ(k)) \rightarrow G \)

shows \( (\prod a) = (\prod \text{Init}(a)) \cdot a(succ(k)) \)

lemma (in semigr0) prod_of_1elem:

assumes \( a: 1 \rightarrow G \)

shows \( (\prod a) = a(0) \)

theorem singleton_prod_top1:

assumes \( \tau \text{ is a topology } \)

shows \( \text{IsAhomeomorphism}( \text{SeqProductTopology}(1,\tau ),\tau ,\{\langle x,x(0)\rangle .\ x\in 1\rightarrow \bigcup \tau \}) \)

Definition of IsAhomeomorphism: \( \text{IsAhomeomorphism}(T,S,f) \equiv \) \( f \in \text{bij}(\bigcup T,\bigcup S) \wedge \text{IsContinuous}(T,S,f) \wedge \text{IsContinuous}(S,T,converse(f)) \)

lemma (in topgroup) sum_list_in_group:

assumes \( n \in nat \) and \( x: succ(n)\rightarrow G \)

shows \( (\sum x) \in G \)

lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)

theorem init_props:

assumes \( n \in nat \) and \( a: succ(n) \rightarrow X \)

shows \( \text{Init}(a) : n \rightarrow X \), \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \), \( a = \text{Append}( \text{Init}(a), a(n)) \)

theorem finite_top_prod_homeo:

assumes \( \tau \text{ is a topology } \) and \( n \in nat \) and \( f = \{\langle x,\langle \text{Init}(x),x(n)\rangle \rangle .\ x \in succ(n)\rightarrow \bigcup \tau \} \) and \( T = \text{SeqProductTopology}(n,\tau ) \) and \( S = \text{SeqProductTopology}(succ(n),\tau ) \)

shows \( \text{IsAhomeomorphism}(S, \text{ProductTopology}(T,\tau ),f) \)

theorem seq_prod_top_is_top:

assumes \( T \text{ is a topology } \)

shows \( \text{SeqProductTopology}(I,T) \text{ is a topology } \) and \( \text{ProductTopBase}(I,T) \text{ is a base for } \text{SeqProductTopology}(I,T) \) and \( \bigcup \text{SeqProductTopology}(I,T) = (I\rightarrow \bigcup T) \)

lemma cart_prod_cont1:

assumes \( \tau _1 \text{ is a topology } \) and \( \tau _2 \text{ is a topology } \) and \( \eta _1 \text{ is a topology } \) and \( f_1:\bigcup \tau _1\rightarrow \bigcup \eta _1 \) and \( \text{IsContinuous}(\tau _1,\eta _1,f_1) \) and \( g = \{\langle p, \langle f_1(\text{fst}(p)),\text{snd}(p)\rangle \rangle .\ p \in \bigcup \tau _1\times \bigcup \tau _2\} \)

shows \( \text{IsContinuous}( \text{ProductTopology}(\tau _1,\tau _2), \text{ProductTopology}(\eta _1,\tau _2),g) \)

lemma ZF_fun_from_tot_val1:

assumes \( x\in X \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \)

lemma (in topgroup) shorter_set_add:

assumes \( n \in nat \) and \( x: succ(succ(n))\rightarrow G \)

shows \( (\sum x) = (\sum \text{Init}(x)) + (x(succ(n))) \)

lemma func1_1_L18:

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

shows \( (h\circ g\circ f)(x) \in D \), \( (h\circ g\circ f)(x) = h(g(f(x))) \)

lemma func_eq:

assumes \( f: X\rightarrow Y \), \( g: X\rightarrow Z \) and \( \forall x\in X.\ f(x) = g(x) \)