[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

hlp



can't proof this plz help.. 

trixbij [T: TYPE]: THEORY
BEGIN 

 V, A, B : VAR set[T] 

 bijection_existence : LEMMA
 FORALL (A,B): (subset?(A,V) AND subset?(B,V) AND
  FORALL (f:[(A)->(B)], g:[(B)->(A)]):(surjective?(f) AND surjective?(g))
   IMPLIES (EXISTS (h:[(A)->(B)]): bijective?(h))) 

END trixbij