| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1024 B |
|
Impressum cayleys.pvs Sprache: PVS |
|||||||||
|
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 ¤ 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.0.12Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
