Quelle  subgroups.pvs

%------------------------------------------------------------------------------
% SubGroups
%
%------------------------------------------------------------------------------

subgroups[T:Type+,*:[T,T->T],one:T]: THEORY

BEGIN
   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING group, group_rew

   G: VAR group[T,*,one]

   subgroup(G): TYPE = { s: set[T] | subset?(s,G) AND group?(s)}

   A,B: VAR set[T]


   pg64_1: LEMMA 
      subgroup?(A,G) AND subgroup?(B,G) 
         IMPLIES subgroup?(intersection(A,B),G)


   IMPORTING normal_subgroups[T,*,one]
 
   center_normal: LEMMA  normal_subgroup?(center(G),G)

END subgroups