| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 40 kB |
|
Quelle index_theorems.pvs Sprache: PVS |
|||||||||
|
index_theorems[T1:Type,T2:Type]: THEORY
% 2/2014 % Summary: If a function f:T1->T2 is surjective, % if t has k elements, and the preimage of t % has a fixed number d of elements for every t % in T2, then T1 has k*d elements and there is a % bijection T1 -> T2 x below(d). This is actually % proved on subsets of T1 and T2 instead of the % full types. BEGIN S1 : VAR set[T1] S2 : VAR set[T2] k,d : VAR posnat finite_index: LEMMA FORALL (f:[(S1)->(S2)]): (EXISTS (b1:[(S2)->below(k)]): bijective?(b1)) AND (FORALL (s2:(S2)): LET PI = inverse_image(f,singleton(s2)) IN EXISTS (b2:[(PI)->below(d)]): bijective?(b2)) IMPLIES ((EXISTS (b:[(S1)->[(S2),below(d)]]): bijective?(b)) AND (EXISTS (b:[(S1)->below(k*d)]): bijective?(b))) END index_theorems ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28