%-------------------------------------------------------------------------
%
% If there are injective (surjective) maps both ways between two sets,
% then the sets are bijective.
%
% For PVS version 3.2. January 18, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% orders: set_antisymmetric[D, R]
%
%-------------------------------------------------------------------------
set_antisymmetric[D: TYPE, R: TYPE]: THEORY
BEGIN
in_closure(f: [D -> R], g: [R -> D], d: D): INDUCTIVE bool =
member(d, complement(image(g, fullset[R]))) OR
(EXISTS (e: D): g(f(e)) = d AND in_closure(f, g, e))
% The Schroeder-Bernstein Theorem
inj_inj_bij: THEOREM
(EXISTS (f: [D -> R]): injective?(f)) AND
(EXISTS (f: [R -> D]): injective?(f))
=> (EXISTS (f: [D -> R]): bijective?(f))
surj_surj_bij: COROLLARY
(EXISTS (f: [D -> R]): surjective?(f)) AND
(EXISTS (f: [R -> D]): surjective?(f))
=> (EXISTS (f: [D -> R]): bijective?(f))
inj_surj_bij: COROLLARY
(EXISTS (f: [D -> R]): injective?(f)) AND
(EXISTS (f: [D -> R]): surjective?(f))
=> (EXISTS (f: [D -> R]): bijective?(f))
END set_antisymmetric
¤ Dauer der Verarbeitung: 0.15 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.
|
