Hi Mario, | If you know of an existing formalization of elementary topology in HOL4 | please let me know, so that I can avoid duplicating work.
Not in HOL4, but in HOL Light there is quite a bit of topology, which might at least serve as inspiration, if not something to port. See the various files here: https://github.com/jrh13/hol-light/tree/master/Multivariate Most of it is rooted in the special case of R^n, but there is one file with purely general topology and metric spaces: https://github.com/jrh13/hol-light/tree/master/Multivariate/metric.ml John. ------------------------------------------------------------------------------ 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
