Hi again ... Suppose I have the following things:
1. An equivalence relation R (|- equivalence R) for type ‘a 2. A ONE-ONE function f (:num->’a). It’s known that all its values are distinct according to R. 3. A finite set J of values of the same type. What theorems could assert the existence of an number N, such that f(N) is not equivalent with any value in the finite set J? Regards, Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
