You can check in "seqTheory" On Thu, Sep 13, 2018 at 3:01 PM 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 >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
