| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 991 B |
|
Quelle card_function.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% finite/infinite properties of functions % % Author: David Lester, Manchester University % % Version 1.0 2/1/05 %------------------------------------------------------------------------------ card_function[D,R:TYPE]: THEORY BEGIN f: VAR [D->R] infinite_bijection: LEMMA bijective?(f) AND is_infinite(fullset[D]) => is_infinite(fullset[R]) finite_bijection: LEMMA bijective?(f) AND is_finite(fullset[D]) => is_finite(fullset[R]) infinite_injection: LEMMA injective?(f) AND is_infinite(fullset[D]) => is_infinite(fullset[R]) finite_injection: LEMMA injective?(f) AND is_finite(fullset[R]) => is_finite(fullset[D]) infinite_surjection: LEMMA surjective?(f) AND is_infinite(fullset[R]) => is_infinite(fullset[D]) finite_surjection: LEMMA surjective?(f) AND is_finite(fullset[D]) => is_finite(fullset[R]) END card_function ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28