| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 935 B |
|
Quelle A_group.pvs Sprache: PVS |
|||||||||
|
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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28