Thanks everyone. I'd like to close the question.
Yesterday I've done a formal proof by constructing an explicit mapping from
the finite set to infinite set (using the Hilbert @ operator), then use
IN_INFINITE_NOT_FINITE to assert the existence of elements from the rest of
infinite map. I also received a shorter proof from mathematics friends by
assuming a mapping from the infinite set to the power of the finite set
(which is still finite), then the non-injectivity will contradict the fact
that all elements in the infinite set are distinct.
My formal proof is quite long, but it's actually the first time I've
successfully done a "pure-math" (but only set-theory gets involved) proof
in HOL4 (previously I was working in a closed theory proving situation that
almost all theorems I needed are those I created by myself). And it was my
35-years birthday yesterday - I see it as a gift to myself:)
Best regards,
Chun
On 5 July 2017 at 12:02, <michael.norr...@data61.csiro.au> wrote:
> A combination of the partition theorems and FINITE_WEAK_ENUMERATE would be
> my guess…
>
> Michael
>
> On 3/7/17, 22:43, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
>
> 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
>
>
>
>
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
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
