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
