| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle homomorphisms.pvs Sprache: PVS |
|||||||||
|
homomorphisms[T1: TYPE,
*: [T1,T1 -> T1], one1: T1, T2: TYPE, o: [T2,T2 -> T2], one2: T2]: THEORY %----------------------------------------------------------------------------- % Experimental theory % % Author: Rick Butler % %----------------------------------------------------------------------------- BEGIN ASSUMING IMPORTING group_def T1_is_group: ASSUMPTION group?[T1,*,one1](fullset[T1]) T2_is_group: ASSUMPTION group?[T2,o,one2](fullset[T2]) ENDASSUMING IMPORTING group[T1,*,one1], group[T2,o,one2] homomorphism?(G1: group[T1,*,one1], G2: group[T2,o,one2], phi: [(G1) -> (G2)]): bool = (FORALL (a,b: (G1)): phi(a*b) = phi(a) o phi(b)) isomorphism?(G1: group[T1,*,one1], G2: group[T2,o,one2], phi: [(G1) -> (G2)]): bool = bijective?(phi) AND homomorphism?(G1,G2,phi) homomorphic?(G1: group[T1,*,one1], G2: group[T2,o,one2]): bool = EXISTS (phi: [(G1) -> (G2)]): homomorphism?(G1,G2,phi) isomorphic?(G1: group[T1,*,one1], G2: group[T2,o,one2]): bool = EXISTS (phi: [(G1) -> (G2)]): isomorphism?(G1,G2,phi) G: VAR group[T1,*,one1] GP: VAR group[T2,o,one2] homomorphism(G,GP): TYPE = {phi:[(G) -> (GP)] | homomorphism?(G,GP,phi)} isomorphism (G,GP): TYPE = {phi:[(G) -> (GP)] | isomorphism?(G,GP,phi)} homo_one: LEMMA FORALL (phi: homomorphism(G,GP)): phi(one1) = one2 kernel(G: group[T1,*,one1], GP: group[T2,o,one2])(phi: homomorphism(G,GP)): subgroup[T1,*,one1](G) = {a: T1 | G(a) AND phi(a) = one2} END homomorphisms ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28