Re: [Hol-info] The "limit" of a ``:'num->'a set`` function?

2018-09-14 Thread Chun Tian (binghe) 
Thanks, now I realized that, to have a meaningful “limit" on a sequence of 
sets, such a sequence must be either increasing or decreasing (f n SUBSET f 
(SUC n), or the other direction), then the “limit” is either BIGUNION (IMAGE f 
univ(:num)) or BIGINTER (IMAGE f univ(:num)).

—Chun

> Il giorno 14 set 2018, alle ore 04:53, michael.norr...@data61.csiro.au ha 
> scritto:
> 
> You don't just want something like
> 
>   BIGUNION (IMAGE f univ(:num))
> 
> ?
> 
> Michael
> 
> On 14/9/18, 05:02, "Chun Tian (binghe)"  wrote:
> 
>Hi,
> 
>I want to express the existence of a function (f :’num -> ‘a set) such 
> that, whenever the number n goes to “infinite”, ``f n`` equals to a given set 
> ``X :’a set``.
> 
>This looks like something in limTheory, but I have nothing to do with real 
> numbers here.
> 
>Does anyone know which definition in HOL4’s existing libraries should I 
> look for?
> 
>Regards,
> 
>Chun Tian
> 
> 
> 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] The "limit" of a ``:'num->'a set`` function?

2018-09-13 Thread Michael.Norrish 
You don't just want something like

   BIGUNION (IMAGE f univ(:num))

?

Michael

On 14/9/18, 05:02, "Chun Tian (binghe)"  wrote:

Hi,

I want to express the existence of a function (f :’num -> ‘a set) such 
that, whenever the number n goes to “infinite”, ``f n`` equals to a given set 
``X :’a set``.

This looks like something in limTheory, but I have nothing to do with real 
numbers here.

Does anyone know which definition in HOL4’s existing libraries should I 
look for?

Regards,

Chun Tian





___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] The "limit" of a ``:'num->'a set`` function?

2018-09-13 Thread Umair Siddique 
You can check  in "seqTheory"

On Thu, Sep 13, 2018 at 3:01 PM Chun Tian (binghe) 
wrote:

> Hi,
>
> I want to express the existence of a function (f :’num -> ‘a set) such
> that, whenever the number n goes to “infinite”, ``f n`` equals to a given
> set ``X :’a set``.
>
> This looks like something in limTheory, but I have nothing to do with real
> numbers here.
>
> Does anyone know which definition in HOL4’s existing libraries should I
> look for?
>
> Regards,
>
> Chun Tian
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] The "limit" of a ``:'num->'a set`` function?

2018-09-13 Thread Chun Tian (binghe) 
Hi,

I want to express the existence of a function (f :’num -> ‘a set) such that, 
whenever the number n goes to “infinite”, ``f n`` equals to a given set ``X :’a 
set``.

This looks like something in limTheory, but I have nothing to do with real 
numbers here.

Does anyone know which definition in HOL4’s existing libraries should I look 
for?

Regards,

Chun Tian




signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info