%-------------------------------------------------------------------------
%
% There is an injective (surjective) map between any pair of sets.
% We have to special case empty sets because, if the range is empty,
% there is NO function from nonempty D to R.
%
% For PVS version 3.2. January 18, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: sets_lemmas[D]
% orders: set_dichotomous[D, R]
%
%-------------------------------------------------------------------------
set_dichotomous[D: TYPE, R: TYPE]: THEORY
% Hide uninteresting intermediate results
EXPORTING injective_or_surjective, injective_dichotomous,
surjective_dichotomous WITH sets_lemmas[D]
BEGIN
IMPORTING sets_lemmas[D], function_inverse_def[D, R]
% ==========================================================================
% Declarations used for the proofs only
% ==========================================================================
subset_injection: TYPE = [S: set[D], (injective?[(S), R])]
d: VAR D
r: VAR R
i, j: VAR subset_injection
injection_order(i, j): bool =
subset?(i`1, j`1) AND (FORALL (d: (i`1)): i`2(d) = j`2(d))
partial_injection_order: JUDGEMENT
injection_order HAS_TYPE (partial_order?[subset_injection])
IMPORTING zorn[subset_injection, injection_order]
% ==========================================================================
% The theorems
% ==========================================================================
injective_or_surjective: THEOREM
(EXISTS (f: [D -> R]): injective?(f)) OR
(EXISTS (f: [D -> R]): surjective?(f)) OR
((EXISTS d: TRUE) AND (FORALL r: FALSE))
injective_dichotomous: COROLLARY
(EXISTS (f: [D -> R]): injective?(f)) OR
(EXISTS (f: [R -> D]): injective?(f))
surjective_dichotomous: COROLLARY
(EXISTS (f: [D -> R]): surjective?(f)) OR
(EXISTS (f: [R -> D]): surjective?(f)) OR
((EXISTS d: TRUE) AND (FORALL r: FALSE)) OR
((FORALL d: FALSE) AND (EXISTS r: TRUE))
END set_dichotomous
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
