*my initial proposition IS NOT TRUE unless the infinite set B has the same
type variable with the ordinals ...
On 12 July 2017 at 23:21, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> 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)
>
>
--
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
