|
%%-------------------** Product of Subgroups **-------------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%----------------------------------------------------------------
products_subgroups[T: TYPE, *: [T,T -> T], one: T]: THEORY
BEGIN
ASSUMING IMPORTING algebra@group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING algebra@normal_subgroups[T,*,one], groups_scaf
G: VAR group[T,*,one]
H,K,N: VAR set[T]
%%% Definitions %%%%%%
prod(H,K): set[T] = {t:T | EXISTS (h:(H), k:(K)): t = h*k}
HK_subgroup: LEMMA FORALL (H, N: subgroup(G)): normal_subgroup?(N,G)
IMPLIES subgroup?(prod(H,N),G)
HK_subgroup_permute: LEMMA FORALL (H, K: subgroup(G)):
subgroup?(prod(H,K),G) IFF prod(H,K) = prod(K,H) ;
H_K_are_subgroups: LEMMA FORALL (H, K: subgroup(G)):
group?(prod(H,K)) IMPLIES
subgroup?(H, prod(H,K)) AND
subgroup?(K, prod(H,K))
END products_subgroups
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
