|
%------------------------------------------------------------------------------
% Groupoids
%
% Author: David Lester, Manchester University & NIA
% Rick Butler
%
% Version 1.0 3/1/02
% Version 1.1 12/3/03 New library structure
% Version 1.2 5/5/04 Reworked for definition files DRL
%------------------------------------------------------------------------------
groupoid[T:Type+,*:[T,T->T]]: THEORY
BEGIN
IMPORTING groupoid_def[T,*]
fullset_is_groupoid: LEMMA groupoid?(fullset[T])
groupoid: NONEMPTY_TYPE = (groupoid?) CONTAINING fullset[T]
G: VAR groupoid
closed : LEMMA FORALL (x,y:(G)): member(x*y,G)
star_closed : LEMMA FORALL (x,y:(G)): G(x*y)
groupoid_is_set: JUDGEMENT groupoid SUBTYPE_OF set[T]
END groupoid
¤ Dauer der Verarbeitung: 0.0 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.
|
