|
cayleys[T: Type+, *:[T,T->T], one:T]: THEORY
%-----------------------------------------------------------------------------
% Experimental theory
%
% Author: Rick Butler
%
%-----------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING group_def[T,*,one], semigroup_def
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING homomorphisms
IMPORTING A_group[T], group
S: VAR semigroup[T,*]
al(S: set[T], a:(S)):[(S) -> T] = (LAMBDA (s:(S)): a*s);
ML(S): set[maps(S)] = {al: [(S) -> (S)] | EXISTS (x: (S)): al = al(S,x)}
cayley_prep: LEMMA FORALL (G: group[T,*,one]): FORALL (a: (G)):
bijective?[(G), (G)](LAMBDA (s: (G)): a * s)
trans_is_group: LEMMA FORALL (G: group[T,*,one]):
group?[maps[T](G), op(G), id(G)](ML(G))
Cayleys: THEOREM FORALL (G: group[T,*,one]):
isomorphic?[T,*,one,maps(G),op(G),id(G)](G, ML(G))
END cayleys
¤ Dauer der Verarbeitung: 0.16 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.
|
