Le 01/06/2015 00:18, Rob Arthan a écrit : > A topological space (in set theory) comprises a pair (X, O) where X is a set > and O, the set of open subsets of X, is a subset of the powerset of X > satisfying > certain conditions. What is the problem in translating this into HOL? This has > already been done for most (or all?) of the various incarnations of HOL.
Sure, there is no difficulty on the mathematical side, and there is no difficulty on the HOL side if everything is written in terms of pairs (X,O) as you suggest. My problem is that I want to use existing theories, in which I do not see how to write a statement on the same set involving different topologies. In Isabelle/HOL/Topological_Spaces.thy, for instance, topological spaces are implemented based on a predicate open from 'a set to bool. Then, for instance, a function f is continuous on X, written continuous f X, if the preimage of any open set is open in X. But this expression, "continuous f X", only contains implicitly the reference to the topology on X. So, my problem is really just a notational problem: how do I define two different predicates 'open' on a set X, how do I write "continuous f X" to refer to one topology in the source and another one in the target, and so on. Of course, I do not want to reinvent the wheel and reprove all statements in a new theory where all topologies at source and goal are given explicitely! Regards, Esseger ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
