Hi Konrad,
Simply because the domain of f is the universe of some ordinals. Actually I
think my initial proposition unless the infinite set B has the same type
variable with the ordinals: ('a ordinal) and ('a set). Now there's a
theorem in ordinalTheory saying that:
[univ_ord_greater_cardinal] Theorem
|- 𝕌(:'a inf) ≺ 𝕌(:'a ordinal)
where (:'a inf) means the sum type: ``:num + 'a``. Reading from right to
left, it says there's no injection from 𝕌(:'a ordinal) to 𝕌(:'a inf). In
another words, for all mappings g, there're x, y IN 𝕌(:'a ordinal) such
that g(x) = g(y) but x <> y.
If my original goal is not true, i.e. for all x IN 𝕌(:'a ordinal), f(x) in
B. then the following mapping:
g(x) = if x < omega then INL (@n. n = &x) else INR f(x)
will map each ('a ordinal) ordinals into B UNION univ(:num), and the part
from non-limit ordinals to univ(:num) is actually a bijection. Now the
result I got from univ_ord_greater_cardinal and the assumption (ONE_ONE f)
are conflict, thus my original goal must be true.
Do you agree?
Regards,
Chun
On 12 July 2017 at 22:53, Konrad Slind <konrad.sl...@gmail.com> wrote:
> I don't know a lot about this (even though I am responsible for
> ordinalTheory) but
> the Axiom of Infinity in HOL asserts the existence of an infinite set
> without
> saying how big it is. How do you know that B is not the same size as the
> domain of f?
>
> Konrad.
>
>
> On Wed, Jul 12, 2017 at 12:50 PM, Chun Tian (binghe) <
> binghe.l...@gmail.com> wrote:
>
>> Hi,
>>
>> I’m using the ordinalTheory and cardinalTheory (in
>> "examples/set-theory/hol_sets”) with the following proposition
>> unprovable:
>>
>> Suppose I have a ONE_ONE function (f :’a ordinal -> ‘b), and an infinite
>> set (B: ‘b set), how can I assert the existence of an ordinal ``n`` such
>> that ``(f n) NOTIN B``?
>>
>> Regards,
>>
>> Chun Tian
>>
>>
>> ------------------------------------------------------------
>> ------------------
>> 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
>>
>>
>
--
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
