Hello.
Is there some established standard as to how to represent a function
with a domain that may be smaller than the type? More specifically, I
need a representation of arbitrary products (i.e.: The “tuples” are
functions from an arbitrary set to the elements of the tuple) to
formalize theorems about product spaces in topology.
If there does not exists a suitable existing formalization, I have no
problem writing it myself, but it would be good to re-use existing work
to avoid wasted time and to have better integration with other (possibly
future) HOL theories that use functions with explicit domain and
products of an arbitrary “indexed collection” of sets.
Thanks.
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
