You don't just want something like
BIGUNION (IMAGE f univ(:num))
?
Michael
On 14/9/18, 05:02, "Chun Tian (binghe)" <binghe.l...@gmail.com> 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
