|
A_group[T: TYPE]: THEORY
%-----------------------------------------------------------------------------
% Experimental theory :
%
% In Chapter 2 Herstein introduces A(S) the group that consists of all
% 1-1 mappings of a nonempty set onto itself.
%
% Author: Rick Butler
%
% the identity function is the identity element
% * is function composition
% inv is the inv function which exists because maps are 1-1
%
%-----------------------------------------------------------------------------
BEGIN
AUTO_REWRITE+ member
S: VAR (nonempty?[T]) %% nonempty set[T]
maps(S: set[T]): TYPE = (bijective?[(S),(S)]) %% 1-1 maps
A(S): set[maps(S)] = fullset[maps(S)]
id(S): maps(S) = identity[(S)]
op(S): [maps(S),maps(S) -> maps(S)] = function_props[(S),(S),(S)].o
IMPORTING group_def
A_is_group: LEMMA group?[maps(S),op(S),id(S)](fullset[maps(S)])
END A_group
¤ Dauer der Verarbeitung: 0.18 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.
|
