> On 31 May 2015, at 14:04, Esseger <[email protected]> wrote: > > Dear all, > > I recently became interested in HOL, especially with Isar which I find > quite fascinating and powerful for "classical" mathematicians. During my > experimentations, there is one construction that I failed completely to > formalize. > > It is best explained by an example. Recall that the discrete topology on > a set is the topology where all sets are open. Then the following > informal propositions are trivial: > > Proposition A: let X be a set. Then the identity, from X with the > discrete topology, to X with any given topology, is continuous. > > Proposition B: Moreover, this property characterizes the discrete topology. > > I fail to formalize Proposition A since I do not see how to define and > use simultaneously several topologies on the same set. (Proposition B is > even more unclear, but less important in my eyes.) Note that the > situation of Proposition A (several topologies on the same space) > happens all the time in mathematics (for instance with the analytic or > Zariski topology on a complex algebraic variety; the topology of norm > convergence, of pointwise strong convergence, and of pointwise weak > convergence, on the space of continuous linear operators on a Banach space). > > So, do you know if there is a standard way to do this kind of stuff in > HOL-like tools?
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. Regards, Rob. ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
