Quelle  set_antisymmetric.pvs

%-------------------------------------------------------------------------
%
%  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 (jamesj@acm.org), 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