IsarMathLib

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

theory Group_ZF_1 imports Group_ZF

begin

In this theory we consider right and left translations and odd functions.

Translations

In this section we consider translations. Translations are maps \(T: G\rightarrow G\) of the form \(T_g (a) = g\cdot a\) or \(T_g (a) = a\cdot g\). We also consider two-dimensional translations \(T_g : G\times G \rightarrow G\times G\), where \(T_g(a,b) = (a\cdot g, b\cdot g)\) or \(T_g(a,b) = (g\cdot a, g\cdot b)\).

For an element \(a\in G\) the right translation is defined a function (set of pairs) such that its value (the second element of a pair) is the value of the group operation on the first element of the pair and \(g\). This looks a bit strange in the raw set notation, when we write a function explicitely as a set of pairs and value of the group operation on the pair \(\langle a,b \rangle\) as \( P\langle a,b\rangle \) instead of the usual infix \(a\cdot b\) or \(a + b\).

definition

\( \text{RightTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle a,g\rangle = b\} \)

A similar definition of the left translation.

definition

\( \text{LeftTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle g,a\rangle = b\} \)

Translations map \(G\) into \(G\). Two dimensional translations map \(G\times G\) into itself.

lemma (in group0) group0_5_L1:

assumes A1: \( g\in G \)

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

from A1 have \( \forall a\in G.\ a\cdot g \in G \) and \( \forall a\in G.\ g\cdot a \in G \) using group_oper_fun, apply_funtype

then show \( \text{RightTranslation}(G,P,g) : G\rightarrow G \), \( \text{LeftTranslation}(G,P,g) : G\rightarrow G \) using RightTranslation_def, LeftTranslation_def, func1_1_L11A

qed

The values of the translations are what we expect.

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 \) using assms, group0_5_L1, RightTranslation_def, LeftTranslation_def, func1_1_L11B

Composition of left translations is a left translation by the product.

lemma (in group0) group0_5_L4:

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

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

from A1 have I: \( h\cdot a\in G \), \( g\cdot h\in G \) using group_oper_fun, apply_funtype

with A1, A2 show \( T_g(T_h(a)) = g\cdot h\cdot a \) using group0_5_L2, group_oper_assoc

with A1, A2, I show \( T_g(T_h(a)) = \text{LeftTranslation}(G,P,g\cdot h)(a) \) using group0_5_L2, group_oper_assoc

qed

Composition of right translations is a right translation by the product.

lemma (in group0) group0_5_L5:

assumes A1: \( g\in G \), \( h\in G \), \( a\in G \) and A2: \( T_g = \text{RightTranslation}(G,P,g) \), \( T_h = \text{RightTranslation}(G,P,h) \)

shows \( T_g(T_h(a)) = a\cdot h\cdot g \), \( T_g(T_h(a)) = \text{RightTranslation}(G,P,h\cdot g)(a) \)proof

from A1 have I: \( a\cdot h\in G \), \( h\cdot g \in G \) using group_oper_fun, apply_funtype

with A1, A2 show \( T_g(T_h(a)) = a\cdot h\cdot g \) using group0_5_L2, group_oper_assoc

with A1, A2, I show \( T_g(T_h(a)) = \text{RightTranslation}(G,P,h\cdot g)(a) \) using group0_5_L2, group_oper_assoc

qed

Point free version of group0_5_L4 and group0_5_L5.

lemma (in group0) trans_comp:

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

shows \( \text{RightTranslation}(G,P,g)\circ \text{RightTranslation}(G,P,h) = \text{RightTranslation}(G,P,h\cdot g) \), \( \text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,h) = \text{LeftTranslation}(G,P,g\cdot h) \)proof

let \( T_g = \text{RightTranslation}(G,P,g) \)

let \( T_h = \text{RightTranslation}(G,P,h) \)

from assms have \( T_g:G\rightarrow G \) and \( T_h:G\rightarrow G \) using group0_5_L1

then have \( T_g\circ T_h:G\rightarrow G \) using comp_fun

moreover

from assms have \( \text{RightTranslation}(G,P,h\cdot g):G\rightarrow G \) using group_op_closed, group0_5_L1

moreover

from assms, \( T_h:G\rightarrow G \) have \( \forall a\in G.\ (T_g\circ T_h)(a) = \text{RightTranslation}(G,P,h\cdot g)(a) \) using comp_fun_apply, group0_5_L5

ultimately show \( T_g\circ T_h = \text{RightTranslation}(G,P,h\cdot g) \) by (rule func_eq )

next

let \( T_g = \text{LeftTranslation}(G,P,g) \)

let \( T_h = \text{LeftTranslation}(G,P,h) \)

from assms have \( T_g:G\rightarrow G \) and \( T_h:G\rightarrow G \) using group0_5_L1

then have \( T_g\circ T_h:G\rightarrow G \) using comp_fun

moreover

from assms have \( \text{LeftTranslation}(G,P,g\cdot h):G\rightarrow G \) using group_op_closed, group0_5_L1

moreover

from assms, \( T_h:G\rightarrow G \) have \( \forall a\in G.\ (T_g\circ T_h)(a) = \text{LeftTranslation}(G,P,g\cdot h)(a) \) using comp_fun_apply, group0_5_L4

ultimately show \( T_g\circ T_h = \text{LeftTranslation}(G,P,g\cdot h) \) by (rule func_eq )

qed

The image of a set under a composition of translations is the same as the image under translation by a product.

lemma (in group0) trans_comp_image:

assumes A1: \( g\in G \), \( h\in G \) and A2: \( 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) \)proof

from A2 have \( T_g(T_h(A)) = (T_g\circ T_h)(A) \) using image_comp

with assms show \( thesis \) using trans_comp

qed

Another form of the image of a set under a composition of translations

lemma (in group0) group0_5_L6:

assumes A1: \( g\in G \), \( h\in G \) and A2: \( A\subseteq G \) and A3: \( T_g = \text{RightTranslation}(G,P,g) \), \( T_h = \text{RightTranslation}(G,P,h) \)

shows \( T_g(T_h(A)) = \{a\cdot h\cdot g.\ a\in A\} \)proof

from A2 have \( \forall a\in A.\ a\in G \)

from A1, A3 have \( T_g : G\rightarrow G \), \( T_h : G\rightarrow G \) using group0_5_L1

with assms, \( \forall a\in A.\ a\in G \) show \( T_g(T_h(A)) = \{a\cdot h\cdot g.\ a\in A\} \) using func1_1_L15C, group0_5_L5

qed

The translation by neutral element is the identity on group.

lemma (in group0) trans_neutral:

shows \( \text{RightTranslation}(G,P,1 ) = id(G) \) and \( \text{LeftTranslation}(G,P,1 ) = id(G) \)proof

have \( \text{RightTranslation}(G,P,1 ):G\rightarrow G \) and \( \forall a\in G.\ \text{RightTranslation}(G,P,1 )(a) = a \) using group0_2_L2, group0_5_L1, group0_5_L2

then show \( \text{RightTranslation}(G,P,1 ) = id(G) \) by (rule indentity_fun )

have \( \text{LeftTranslation}(G,P,1 ):G\rightarrow G \) and \( \forall a\in G.\ \text{LeftTranslation}(G,P,1 )(a) = a \) using group0_2_L2, group0_5_L1, group0_5_L2

then show \( \text{LeftTranslation}(G,P,1 ) = id(G) \) by (rule indentity_fun )

qed

Translation by neutral element does not move sets.

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

Composition of translations by an element and its inverse is identity.

lemma (in group0) trans_comp_id:

assumes \( g\in G \)

shows \( \text{RightTranslation}(G,P,g)\circ \text{RightTranslation}(G,P,g^{-1}) = id(G) \) and \( \text{RightTranslation}(G,P,g^{-1})\circ \text{RightTranslation}(G,P,g) = id(G) \) and \( \text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,g^{-1}) = id(G) \) and \( \text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G) \) using assms, inverse_in_group, trans_comp, group0_2_L6, trans_neutral

Translations are bijective.

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

from assms have \( \text{RightTranslation}(G,P,g):G\rightarrow G \) and \( \text{RightTranslation}(G,P,g^{-1}):G\rightarrow G \) and \( \text{RightTranslation}(G,P,g)\circ \text{RightTranslation}(G,P,g^{-1}) = id(G) \), \( \text{RightTranslation}(G,P,g^{-1})\circ \text{RightTranslation}(G,P,g) = id(G) \) using inverse_in_group, group0_5_L1, trans_comp_id

then show \( \text{RightTranslation}(G,P,g) \in \text{bij}(G,G) \) using fg_imp_bijective

from assms have \( \text{LeftTranslation}(G,P,g):G\rightarrow G \) and \( \text{LeftTranslation}(G,P,g^{-1}):G\rightarrow G \) and \( \text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,g^{-1}) = id(G) \), \( \text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G) \) using inverse_in_group, group0_5_L1, trans_comp_id

then show \( \text{LeftTranslation}(G,P,g) \in \text{bij}(G,G) \) using fg_imp_bijective

qed

Converse of a translation is translation by the inverse.

lemma (in group0) trans_conv_inv:

assumes \( g\in G \)

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

from assms have \( \text{RightTranslation}(G,P,g) \in \text{bij}(G,G) \), \( \text{RightTranslation}(G,P,g^{-1}) \in \text{bij}(G,G) \) and \( \text{LeftTranslation}(G,P,g) \in \text{bij}(G,G) \), \( \text{LeftTranslation}(G,P,g^{-1}) \in \text{bij}(G,G) \) using trans_bij, inverse_in_group

moreover

from assms have \( \text{RightTranslation}(G,P,g^{-1})\circ \text{RightTranslation}(G,P,g) = id(G) \) and \( \text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G) \) and \( \text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,g^{-1}) = id(G) \) and \( \text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G) \) using trans_comp_id

ultimately show \( converse( \text{RightTranslation}(G,P,g)) = \text{RightTranslation}(G,P,g^{-1}) \) and \( converse( \text{LeftTranslation}(G,P,g)) = \text{LeftTranslation}(G,P,g^{-1}) \) and \( \text{LeftTranslation}(G,P,g) = converse( \text{LeftTranslation}(G,P,g^{-1})) \) and \( \text{RightTranslation}(G,P,g) = converse( \text{RightTranslation}(G,P,g^{-1})) \) using comp_id_conv

qed

The image of a set by translation is the same as the inverse image by by the inverse element translation.

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

Another way of looking at translations is that they are sections of the group operation.

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

let \( T = \text{RightTranslation}(G,P,g) \)

let \( F = \text{Fix2ndVar}(P,g) \)

from assms have \( T: G\rightarrow G \) and \( F: G\rightarrow G \) using group0_5_L1, group_oper_fun, fix_2nd_var_fun

moreover

from assms have \( \forall a\in G.\ T(a) = F(a) \) using group0_5_L2, group_oper_fun, fix_var_val

ultimately show \( T = F \) by (rule func_eq )

next

let \( T = \text{LeftTranslation}(G,P,g) \)

let \( F = \text{Fix1stVar}(P,g) \)

from assms have \( T: G\rightarrow G \) and \( F: G\rightarrow G \) using group0_5_L1, group_oper_fun, fix_1st_var_fun

moreover

from assms have \( \forall a\in G.\ T(a) = F(a) \) using group0_5_L2, group_oper_fun, fix_var_val

ultimately show \( T = F \) by (rule func_eq )

qed

A lemma demonstrating what is the left translation of a set

lemma (in group0) ltrans_image:

assumes A1: \( V\subseteq G \) and A2: \( x\in G \)

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

from assms have \( \text{LeftTranslation}(G,P,x)(V) = \{ \text{LeftTranslation}(G,P,x)(v).\ v\in V\} \) using group0_5_L1, func_imagedef

moreover

from assms have \( \forall v\in V.\ \text{LeftTranslation}(G,P,x)(v) = x\cdot v \) using group0_5_L2

ultimately show \( thesis \)

qed

A lemma demonstrating what is the right translation of a set

lemma (in group0) rtrans_image:

assumes A1: \( V\subseteq G \) and A2: \( x\in G \)

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

from assms have \( \text{RightTranslation}(G,P,x)(V) = \{ \text{RightTranslation}(G,P,x)(v).\ v\in V\} \) using group0_5_L1, func_imagedef

moreover

from assms have \( \forall v\in V.\ \text{RightTranslation}(G,P,x)(v) = v\cdot x \) using group0_5_L2

ultimately show \( thesis \)

qed

Right and left translations of a set are subsets of the group. Interestingly, we do not have to assume the set is a subset of the group.

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

from assms have \( \text{LeftTranslation}(G,P,x):G\rightarrow G \) and \( \text{RightTranslation}(G,P,x):G\rightarrow G \) using group0_5_L1

then show \( \text{LeftTranslation}(G,P,x)(V) \subseteq G \) and \( \text{RightTranslation}(G,P,x)(V) \subseteq G \) using func1_1_L6(2)

qed

A technical lemma about solving equations with translations.

lemma (in group0) ltrans_inv_in:

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

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

have \( x\in G \)proof

from A2 have \( \text{LeftTranslation}(G,P,y):G\rightarrow G \) using group0_5_L1

then have \( \text{LeftTranslation}(G,P,y)( \text{GroupInv}(G,P)(V)) \subseteq G \) using func1_1_L6

with A3 show \( x\in G \)

qed

have \( \exists v\in V.\ x = y\cdot v^{-1} \)proof

have \( \text{GroupInv}(G,P): G\rightarrow G \) using groupAssum, group0_2_T2

with assms obtain \( z \) where \( z \in \text{GroupInv}(G,P)(V) \) and \( x = y\cdot z \) using func1_1_L6, ltrans_image

with A1, \( \text{GroupInv}(G,P): G\rightarrow G \) show \( thesis \) using func_imagedef

qed

then obtain \( v \) where \( v\in V \) and \( x = y\cdot v^{-1} \)

with A1, A2 have \( y = x\cdot v \) using inv_cancel_two

with assms, \( x\in G \), \( v\in V \) show \( thesis \) using ltrans_image

qed

We can look at the result of interval arithmetic operation as union of left translated sets.

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

from assms have I: \( (P \text{ lifted to subsets of } G)\langle A,B\rangle = \{a\cdot b .\ \langle a,b\rangle \in A\times B\} \) using group_oper_fun, lift_subsets_explained

{

fix \( c \)

assume \( c \in (P \text{ lifted to subsets of } G)\langle A,B\rangle \)

with I obtain \( a \) \( b \) where \( c = a\cdot b \) and \( a\in A \), \( b\in B \)

hence \( c \in \{a\cdot b.\ b\in B\} \)

moreover

from assms, \( a\in A \) have \( \text{LeftTranslation}(G,P,a)(B) = \{a\cdot b.\ b\in B\} \) using ltrans_image

ultimately have \( c \in \text{LeftTranslation}(G,P,a)(B) \)

with \( a\in A \) have \( c \in (\bigcup a\in A.\ \text{LeftTranslation}(G,P,a)(B)) \)

}

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

{

fix \( c \)

assume \( c \in (\bigcup a\in A.\ \text{LeftTranslation}(G,P,a)(B)) \)

then obtain \( a \) where \( a\in A \) and \( c \in \text{LeftTranslation}(G,P,a)(B) \)

moreover

from assms, \( a\in A \) have \( \text{LeftTranslation}(G,P,a)(B) = \{a\cdot b.\ b\in B\} \) using ltrans_image

ultimately obtain \( b \) where \( b\in B \) and \( c = a\cdot b \)

with I, \( a\in A \) have \( c \in (P \text{ lifted to subsets of } G)\langle A,B\rangle \)

}

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

qed

The right translation version of image_ltrans_union The proof follows the same schema.

lemma (in group0) image_rtrans_union:

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

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

from assms have I: \( (P \text{ lifted to subsets of } G)\langle A,B\rangle = \{a\cdot b .\ \langle a,b\rangle \in A\times B\} \) using group_oper_fun, lift_subsets_explained

{

fix \( c \)

assume \( c \in (P \text{ lifted to subsets of } G)\langle A,B\rangle \)

with I obtain \( a \) \( b \) where \( c = a\cdot b \) and \( a\in A \), \( b\in B \)

hence \( c \in \{a\cdot b.\ a\in A\} \)

moreover

from assms, \( b\in B \) have \( \text{RightTranslation}(G,P,b)(A) = \{a\cdot b.\ a\in A\} \) using rtrans_image

ultimately have \( c \in \text{RightTranslation}(G,P,b)(A) \)

with \( b\in B \) have \( c \in (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \)

}

thus \( (P \text{ lifted to subsets of } G)\langle A,B\rangle \subseteq (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \)

{

fix \( c \)

assume \( c \in (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \)

then obtain \( b \) where \( b\in B \) and \( c \in \text{RightTranslation}(G,P,b)(A) \)

moreover

from assms, \( b\in B \) have \( \text{RightTranslation}(G,P,b)(A) = \{a\cdot b.\ a\in A\} \) using rtrans_image

ultimately obtain \( a \) where \( a\in A \) and \( c = a\cdot b \)

with I, \( b\in B \) have \( c \in (P \text{ lifted to subsets of } G)\langle A,B\rangle \)

}

thus \( (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \subseteq (P \text{ lifted to subsets of } G)\langle A,B\rangle \)

qed

If the neutral element belongs to a set, then an element of group belongs the translation of that set.

lemma (in group0) neut_trans_elem:

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

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

from assms have \( g\cdot 1 \in \text{LeftTranslation}(G,P,g)(A) \) using ltrans_image

with A1 show \( g \in \text{LeftTranslation}(G,P,g)(A) \) using group0_2_L2

from assms have \( 1 \cdot g \in \text{RightTranslation}(G,P,g)(A) \) using rtrans_image

with A1 show \( g \in \text{RightTranslation}(G,P,g)(A) \) using group0_2_L2

qed

The neutral element belongs to the translation of a set by the inverse of an element that belongs to it.

lemma (in group0) elem_trans_neut:

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

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

from assms have ginv: \( g^{-1} \in G \) using inverse_in_group

with assms have \( g^{-1}\cdot g \in \text{LeftTranslation}(G,P,g^{-1})(A) \) using ltrans_image

moreover

from assms have \( g^{-1}\cdot g = 1 \) using group0_2_L6

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

from ginv, assms have \( g\cdot g^{-1} \in \text{RightTranslation}(G,P,g^{-1})(A) \) using rtrans_image

moreover

from assms have \( g\cdot g^{-1} = 1 \) using group0_2_L6

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

qed

Odd functions

This section is about odd functions.

Odd functions are those that commute with the group inverse: \(f(a^{-1}) = (f(a))^{-1}.\)

definition

\( \text{IsOdd}(G,P,f) \equiv (\forall a\in G.\ f( \text{GroupInv}(G,P)(a)) = \text{GroupInv}(G,P)(f(a)) ) \)

Let's see the definition of an odd function in a more readable notation.

lemma (in group0) group0_6_L1:

shows \( \text{IsOdd}(G,P,p) \longleftrightarrow ( \forall a\in G.\ p(a^{-1}) = (p(a))^{-1} ) \) using IsOdd_def

We can express the definition of an odd function in two ways.

lemma (in group0) group0_6_L2:

assumes A1: \( p : G\rightarrow G \)

shows \( (\forall a\in G.\ p(a^{-1}) = (p(a))^{-1}) \longleftrightarrow (\forall a\in G.\ (p(a^{-1}))^{-1} = p(a)) \)proof

assume \( \forall a\in G.\ p(a^{-1}) = (p(a))^{-1} \)

with A1 show \( \forall a\in G.\ (p(a^{-1}))^{-1} = p(a) \) using apply_funtype, group_inv_of_inv

next

assume A2: \( \forall a\in G.\ (p(a^{-1}))^{-1} = p(a) \)

{

fix \( a \)

assume \( a\in G \)

with A1, A2 have \( p(a^{-1}) \in G \) and \( ((p(a^{-1}))^{-1})^{-1} = (p(a))^{-1} \) using apply_funtype, inverse_in_group

then have \( p(a^{-1}) = (p(a))^{-1} \) using group_inv_of_inv

}

then show \( \forall a\in G.\ p(a^{-1}) = (p(a))^{-1} \)

qed

Subgroups and interval arithmetic

The section Binary operations in the func_ZF theory defines the notion of "lifting operation to subsets". In short, every binary operation \(f:X\times X \longrightarrow X \) on a set \(X\) defines an operation on the subsets of \(X\) defined by \(F(A,B) = \{ f\langle x,y \rangle | x\in A, y\in B\}\). In the group context using multiplicative notation we can write this as \(H\cdot K = \{ x\cdot y | x\in A, y\in B\}\). Similarly we can define \(H^{-1}=\{ x^{-1} | x\in H\}\). In this section we study properties of these derived operations and how they relate to the concept of subgroups.

The next locale extends the groups0 locale with notation related to interval arithmetics.

locale group4 = group0 +

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

defines \( A^{-1} \equiv \text{GroupInv}(G,P)(A) \)

The next lemma shows a somewhat more explicit way of defining the product of two subsets of a group.

lemma (in group4) interval_prod:

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

shows \( A\cdot B = \{x\cdot y.\ \langle x,y\rangle \in A\times B\} \) using assms, group_oper_fun, lift_subsets_explained

Product of elements of subsets of the group is in the set product of those subsets

lemma (in group4) interval_prod_el:

assumes \( A\subseteq G \), \( B\subseteq G \), \( x\in A \), \( y\in B \)

shows \( x\cdot y \in A\cdot B \) using assms, interval_prod

An alternative definition of a group inverse of a set.

lemma (in group4) interval_inv:

assumes \( A\subseteq G \)

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

from groupAssum have \( \text{GroupInv}(G,P):G\rightarrow G \) using group0_2_T2

with assms show \( A^{-1} = \{x^{-1}.\ x\in A\} \) using func_imagedef

qed

Group inverse of a set is a subset of the group. Interestingly we don't need to assume the set is a subset of the group.

lemma (in group4) interval_inv_cl:

shows \( A^{-1} \subseteq G \)proof

from groupAssum have \( \text{GroupInv}(G,P):G\rightarrow G \) using group0_2_T2

then show \( A^{-1} \subseteq G \) using func1_1_L6(2)

qed

The product of two subsets of a group is a subset of the group.

lemma (in group4) interval_prod_closed:

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

shows \( A\cdot B \subseteq G \)proof

fix \( z \)

assume \( z \in A\cdot B \)

with assms obtain \( x \) \( y \) where \( x\in A \), \( y\in B \), \( z=x\cdot y \) using interval_prod

with assms show \( z\in G \) using group_op_closed

qed

The product of sets operation is associative.

lemma (in group4) interval_prod_assoc:

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

shows \( A\cdot B\cdot C = A\cdot (B\cdot C) \)proof

from groupAssum have \( (P \text{ lifted to subsets of } G) \text{ is associative on } Pow(G) \) unfolding IsAgroup_def, IsAmonoid_def using lift_subset_assoc

with assms show \( thesis \) unfolding IsAssociative_def

qed

A simple rearrangement following from associativity of the product of sets operation.

lemma (in group4) interval_prod_rearr1:

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

shows \( A\cdot B\cdot (C\cdot D) = A\cdot (B\cdot C)\cdot D \)proof

from assms(1,2) have \( A\cdot B \subseteq G \) using interval_prod_closed

with assms(3,4) have \( A\cdot B\cdot (C\cdot D) = A\cdot B\cdot C\cdot D \) using interval_prod_assoc

also

from assms(1,2,3) have \( A\cdot B\cdot C\cdot D = A\cdot (B\cdot C)\cdot D \) using interval_prod_assoc

finally show \( thesis \)

qed

A subset \(A\) of the group is closed with respect to the group operation iff \(A\cdot A \subseteq A\).

lemma (in group4) subset_gr_op_cl:

assumes \( A\subseteq G \)

shows \( (A \text{ is closed under } P) \longleftrightarrow A\cdot A \subseteq A \)proof

assume \( A \text{ is closed under } P \)

{

fix \( z \)

assume \( z \in A\cdot A \)

with assms obtain \( x \) \( y \) where \( x\in A \), \( y\in A \) and \( z=x\cdot y \) using interval_prod

with \( A \text{ is closed under } P \) have \( z\in A \) unfolding IsOpClosed_def

}

thus \( A\cdot A \subseteq A \)

next

assume \( A\cdot A \subseteq A \)

{

fix \( x \) \( y \)

assume \( x\in A \), \( y\in A \)

with assms have \( x\cdot y \in A\cdot A \) using interval_prod

with \( A\cdot A \subseteq A \) have \( x\cdot y \in A \)

}

then show \( A \text{ is closed under } P \) unfolding IsOpClosed_def

qed

Inverse and square of a subgroup is this subgroup.

lemma (in group4) subgroup_inv_sq:

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

shows \( H^{-1} = H \) and \( H\cdot H = H \)proof

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

with assms show \( H^{-1} \subseteq H \) using interval_inv, group0_3_T3A

{

fix \( x \)

assume \( x\in H \)

with assms have \( (x^{-1})^{-1} \in \{y^{-1}.\ y\in H\} \) using group0_3_T3A

moreover

from \( x\in H \), \( H\subseteq G \) have \( (x^{-1})^{-1} = x \) using group_inv_of_inv

ultimately have \( x \in \{y^{-1}.\ y\in H\} \)

with \( H\subseteq G \) have \( x \in H^{-1} \) using interval_inv

}

thus \( H \subseteq H^{-1} \)

from assms have \( H \text{ is closed under } P \) using group0_3_L6 unfolding IsOpClosed_def

with assms have \( H\cdot H \subseteq H \) using subset_gr_op_cl, group0_3_L2

moreover {

fix \( x \)

assume \( x\in H \)

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

from assms, \( H\subseteq G \), \( x\in H \) have \( x\cdot 1 \in H\cdot H \) using group0_3_L5, interval_prod

with \( x\in G \) have \( x \in H\cdot H \) using group0_2_L2

}

hence \( H \subseteq H\cdot H \)

ultimately show \( H\cdot H = H \)

qed

Inverse of a product two sets is a product of inverses with the reversed order.

lemma (in group4) interval_prod_inv:

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

shows \( (A\cdot B)^{-1} = \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \), \( (A\cdot B)^{-1} = \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \), \( (A\cdot B)^{-1} = (B^{-1})\cdot (A^{-1}) \)proof

from assms have \( (A\cdot B) \subseteq G \) using interval_prod_closed

then have I: \( (A\cdot B)^{-1} = \{z^{-1}.\ z\in A\cdot B\} \) using interval_inv

show II: \( (A\cdot B)^{-1} = \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)proof

{

fix \( p \)

assume \( p \in (A\cdot B)^{-1} \)

with I obtain \( z \) where \( p=z^{-1} \) and \( z\in A\cdot B \)

with assms obtain \( x \) \( y \) where \( \langle x,y\rangle \in A\times B \) and \( z=x\cdot y \) using interval_prod

with \( p=z^{-1} \) have \( p\in \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)

}

thus \( (A\cdot B)^{-1} \subseteq \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)

{

fix \( p \)

assume \( p\in \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)

then obtain \( x \) \( y \) where \( x\in A \), \( y\in B \) and \( p=(x\cdot y)^{-1} \)

with assms, \( (A\cdot B) \subseteq G \) have \( p\in (A\cdot B)^{-1} \) using interval_prod, interval_inv

}

thus \( \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \subseteq (A\cdot B)^{-1} \)

qed

have \( \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} = \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)proof

{

fix \( p \)

assume \( p \in \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)

then obtain \( x \) \( y \) where \( x\in A \), \( y\in B \) and \( p=(x\cdot y)^{-1} \)

with assms have \( y^{-1}\cdot x^{-1} = (x\cdot y)^{-1} \) using group_inv_of_two

with \( p=(x\cdot y)^{-1} \) have \( p = y^{-1}\cdot x^{-1} \)

with \( x\in A \), \( y\in B \) have \( p\in \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)

}

thus \( \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \subseteq \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)

{

fix \( p \)

assume \( p\in \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)

then obtain \( x \) \( y \) where \( x\in A \), \( y\in B \) and \( p=y^{-1}\cdot x^{-1} \)

with assms have \( p = (x\cdot y)^{-1} \) using group_inv_of_two

with \( x\in A \), \( y\in B \) have \( p \in \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)

}

thus \( \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \subseteq \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)

qed

with II show III: \( (A\cdot B)^{-1} = \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)

have \( \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} = (B^{-1})\cdot (A^{-1}) \)proof

{

fix \( p \)

assume \( p\in \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)

then obtain \( x \) \( y \) where \( x\in A \), \( y\in B \) and \( p=y^{-1}\cdot x^{-1} \)

with assms have \( y^{-1} \in (B^{-1}) \) and \( x^{-1} \in (A^{-1}) \) using interval_inv

with \( p=y^{-1}\cdot x^{-1} \) have \( p \in (B^{-1})\cdot (A^{-1}) \) using interval_inv_cl, interval_prod

}

thus \( \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \subseteq (B^{-1})\cdot (A^{-1}) \)

{

fix \( p \)

assume \( p \in (B^{-1})\cdot (A^{-1}) \)

then obtain \( y \) \( x \) where \( y\in B^{-1} \), \( x\in A^{-1} \) and \( p=y\cdot x \) using interval_inv_cl, interval_prod

with assms obtain \( x_1 \) \( y_1 \) where \( x_1 \in A \), \( y_1 \in B \) and \( x=x_1^{-1} \), \( y=y_1^{-1} \) using interval_inv

with \( p=y\cdot x \) have \( p \in \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)

}

thus \( (B^{-1})\cdot (A^{-1}) \subseteq \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)

qed

with III show \( (A\cdot B)^{-1} = (B^{-1})\cdot (A^{-1}) \)

qed

If \(H,K\) are subgroups then \(H\cdot K\) is a subgroup iff \(H\cdot K = K\cdot H\).

theorem (in group4) prod_subgr_subgr:

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

shows \( \text{IsAsubgroup}(H\cdot K,P) \longleftrightarrow H\cdot K = K\cdot H \)proof

assume \( \text{IsAsubgroup}(H\cdot K,P) \)

then have \( (H\cdot K)^{-1} = H\cdot K \) using subgroup_inv_sq(1)

with assms show \( H\cdot K = K\cdot H \) using group0_3_L2, interval_prod_inv, subgroup_inv_sq(1)

next

from assms have \( H\subseteq G \) and \( K\subseteq G \) using group0_3_L2

have I: \( H\cdot K \neq 0 \)proof

let \( x = 1 \)

let \( y = 1 \)

from assms have \( x\cdot y \in (H\cdot K) \) using group0_3_L5, group0_3_L2, interval_prod

thus \( thesis \)

qed

from \( H\subseteq G \), \( K\subseteq G \) have II: \( H\cdot K \subseteq G \) using interval_prod_closed

assume \( H\cdot K = K\cdot H \)

have III: \( (H\cdot K)\text{ is closed under } P \)proof

have \( (H\cdot K)\cdot (H\cdot K) = H\cdot K \)proof

from \( H\subseteq G \), \( K\subseteq G \) have \( (H\cdot K)\cdot (H\cdot K) = H\cdot (K\cdot H)\cdot K \) using interval_prod_rearr1

also

from \( H\cdot K = K\cdot H \) have \( .\ .\ .\ = H\cdot (H\cdot K)\cdot K \)

also

from \( H\subseteq G \), \( K\subseteq G \) have \( .\ .\ .\ = (H\cdot H)\cdot (K\cdot K) \) using interval_prod_rearr1

also

from assms have \( .\ .\ .\ = H\cdot K \) using subgroup_inv_sq(2)

finally show \( thesis \)

qed

with \( H\cdot K \subseteq G \) show \( thesis \) using subset_gr_op_cl

qed

have IV: \( \forall x \in H\cdot K.\ x^{-1} \in H\cdot K \)proof

{

fix \( x \)

assume \( x \in H\cdot K \)

with \( H\cdot K \subseteq G \) have \( x^{-1} \in (H\cdot K)^{-1} \) using interval_inv

with assms, \( H\subseteq G \), \( K\subseteq G \), \( H\cdot K = K\cdot H \) have \( x^{-1} \in H\cdot K \) using interval_prod_inv, subgroup_inv_sq(1)

}

thus \( thesis \)

qed

from I, II, III, IV show \( \text{IsAsubgroup}(H\cdot K,P) \) using group0_3_T3

qed

end

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

Definition of RightTranslation: \( \text{RightTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle a,g\rangle = b\} \)

Definition of LeftTranslation: \( \text{LeftTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle g,a\rangle = b\} \)

lemma func1_1_L11A:

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

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

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 func1_1_L11B:

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

shows \( f(x) = b(x) \)

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

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

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

lemma (in group0) group0_5_L5:

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

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

lemma func_eq:

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

shows \( f = g \)

lemma (in group0) group0_5_L4:

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

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

lemma (in group0) trans_comp:

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

lemma func1_1_L15C:

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

shows \( g(f(A)) = \{g(f(x)).\ x\in A\} \), \( g(f(A)) = (g\circ f)(A) \)

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 indentity_fun:

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

shows \( f = id(X) \)

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

assumes \( x\in G \)

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

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_comp_id:

assumes \( g\in G \)

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 comp_id_conv:

assumes \( a \in \text{bij}(A,B) \), \( b \in \text{bij}(B,A) \) and \( b\circ a = id(A) \)

shows \( a = converse(b) \) and \( b = converse(a) \)

lemma (in group0) trans_conv_inv:

assumes \( g\in G \)

lemma vimage_converse: shows \( r^{-1}(A) = converse(r)(A) \)

lemma fix_2nd_var_fun:

assumes \( f : X\times Y \rightarrow Z \) and \( y\in Y \)

shows \( \text{Fix2ndVar}(f,y) : X \rightarrow Z \)

lemma fix_var_val:

assumes \( f : X\times Y \rightarrow Z \) and \( x\in X \), \( y\in Y \)

shows \( \text{Fix1stVar}(f,x)(y) = f\langle x,y\rangle \), \( \text{Fix2ndVar}(f,y)(x) = f\langle x,y\rangle \)

lemma fix_1st_var_fun:

assumes \( f : X\times Y \rightarrow Z \) and \( x\in X \)

shows \( \text{Fix1stVar}(f,x) : Y \rightarrow Z \)

lemma func_imagedef:

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

shows \( f(A) = \{f(x).\ x \in A\} \)

lemma func1_1_L6:

assumes \( f:X\rightarrow Y \)

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

lemma func1_1_L6:

assumes \( f:X\rightarrow Y \)

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

theorem group0_2_T2:

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

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

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

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

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

Definition of IsOdd: \( \text{IsOdd}(G,P,f) \equiv (\forall a\in G.\ f( \text{GroupInv}(G,P)(a)) = \text{GroupInv}(G,P)(f(a)) ) \)

lemma (in group0) group_inv_of_inv:

assumes \( a\in G \)

shows \( a = (a^{-1})^{-1} \)

lemma (in group4) interval_prod:

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

shows \( A\cdot B = \{x\cdot y.\ \langle x,y\rangle \in A\times B\} \)

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 lift_subset_assoc:

assumes \( f \text{ is associative on } X \) and \( F = f \text{ lifted to subsets of } X \)

shows \( F \text{ is associative on } Pow(X) \)

Definition of IsAssociative: \( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \) \( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \) \( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)

lemma (in group4) interval_prod_closed:

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

shows \( A\cdot B \subseteq G \)

lemma (in group4) interval_prod_assoc:

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

shows \( A\cdot B\cdot C = A\cdot (B\cdot C) \)

Definition of IsOpClosed: \( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)

lemma (in group0) group0_3_L2:

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

shows \( H \subseteq G \)

lemma (in group4) interval_inv:

assumes \( A\subseteq G \)