IsarMathLib

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

theory TopologicalGroup_ZF imports Topology_ZF_2 Group_ZF_1
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,\tau)\) such that \(\tau\) 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 \tau\) instead of \(G\) and say that the pair of sets \((\bigcup \tau , f)\) is a group. This way our definition of being a topological group is a statement about two sets: the topology \(\tau\) and the group operation \(f\) on \(\bigcup \tau\). Since the domain of the group operation is \(G\times G\), the pair of topologies in which \(f\) is supposed to be continuous is \(\tau\) and the product topology on \(G\times G\).

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

Definition

\( \text{IsAtopologicalGroup}(\tau ,f) \equiv (\tau \text{ is a topology }) \wedge \text{IsAgroup}(\bigcup \tau ,f) \wedge \) \( \text{IsContinuous}( \text{ProductTopology}(\tau ,\tau ),\tau ,f) \wedge \) \( \text{IsContinuous}(\tau ,\tau , \text{GroupInv}(\bigcup \tau ,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)\} \)

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 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 \)proof
from assms have \( \text{GroupInv}(G,f)(g) \in G \) using group0_valid_in_tgroup , inverse_in_group
thus \( thesis \)
qed

Zero is in the group.

lemma (in topgroup) zero_in_tgroup:

shows \( 0 \in G \)proof
have \( \text{TheNeutralElement}(G,f) \in G \) using group0_valid_in_tgroup , group0_2_L2
then show \( 0 \in G \)
qed

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_assocA

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_valid_in_tgroup , 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_valid_in_tgroup , 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_valid_in_tgroup , 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 group0_valid_in_tgroup , restr_inv_onto
moreover
from A1 have \( \text{GroupInv}(H,f_H) = g \) using group0_valid_in_tgroup , 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 \) and \( A + B = f(A\times B) \), \( A + B = (\bigcup x\in A.\ x + B) \)proof
from assms show \( A + B \subseteq G \) and \( A + B = f(A\times B) \) using topgroup_f_binop , lift_subsets_explained
from assms show \( A + B = (\bigcup x\in A.\ x + B) \) using group0_valid_in_tgroup , image_ltrans_union
qed

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 , group0_valid_in_tgroup , 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 , group0_valid_in_tgroup , 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 , group0_valid_in_tgroup , trans_bij , trans_cont , open_tr_open , bij_cont_open_homeo

Translations preserve interior.

lemma (in topgroup) trans_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

Inverse of an open set is open.

lemma (in topgroup) open_inv_open:

assumes \( V\in T \)

shows \( -V \in T \) using assms , group0_valid_in_tgroup , 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 group0_valid_in_tgroup , 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 sppace 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 belongs to the interior of any neighboorhood of zero translated by that element.

lemma (in topgroup) elem_in_int_trans:

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

shows \( g \in int(g + H) \)proof
from A2 have \( 0 \in int(H) \) and \( int(H) \subseteq G \) using Top_2_L2
with A1 have \( g \in g + int(H) \) using group0_valid_in_tgroup , neut_trans_elem
with assms show \( thesis \) using trans_interior
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 group0_valid_in_tgroup , 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

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 group0_valid_in_tgroup , elem_trans_neut , Top_2_L3
qed
ultimately 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 , trans_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_trans , 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 group0_valid_in_tgroup , 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
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
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 group0_valid_in_tgroup , ltrans_inv_in
with \( U\in T \), \( x\in G \) show \( y\in U \) using neg_in_tgroup , group0_valid_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
end
Definition of IsAtopologicalGroup: \( \text{IsAtopologicalGroup}(\tau ,f) \equiv (\tau \text{ is a topology }) \wedge \text{IsAgroup}(\bigcup \tau ,f) \wedge \) \( \text{IsContinuous}( \text{ProductTopology}(\tau ,\tau ),\tau ,f) \wedge \) \( \text{IsContinuous}(\tau ,\tau , \text{GroupInv}(\bigcup \tau ,f)) \)
lemma (in topgroup) group0_valid_in_tgroup: shows \( group0(G,f) \)
lemma (in group0) inverse_in_group: assumes \( x\in G \) shows \( x^{-1}\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)) \)
theorem Top_1_4_T1: assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) shows \( \text{ProductTopology}(T,S) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } \text{ProductTopology}(T,S) \), \( \bigcup \text{ProductTopology}(T,S) = \bigcup T \times \bigcup S \)
lemma (in group0) group_oper_assocA: 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 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) 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 \)
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) \)
lemma (in topgroup) trans_interior: assumes \( g\in G \) and \( A\subseteq G \) shows \( g + int(A) = int(g + A) \)
lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
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) \)
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 topgroup) neg_neigh_neigh: assumes \( H \in \mathcal{N}_0 \) shows \( -H \in \mathcal{N}_0 \)
lemma (in topgroup) elem_in_int_trans: assumes \( g\in G \) and \( H \in \mathcal{N}_0 \) shows \( g \in int(g + H) \)
lemma (in topology0) 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 func1_1_L8: assumes \( A\subseteq B \) shows \( f(A)\subseteq f(B) \)
lemma (in topgroup) interval_add: assumes \( A\subseteq G \), \( B\subseteq G \) shows \( A + B \subseteq G \) and \( A + B = f(A\times B) \), \( A + B = (\bigcup x\in A.\ x + B) \)
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 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 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) \)
89
110
19
19