[Hol-info] Choosing an element from an infinite set according to an equivalence relation and a finite set?

[Chun Tian (binghe)]

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)]

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

A combination of the partition theorems and FINITE_WEAK_ENUMERATE would be
my guess

Michael
Hi again ...
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