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? Best, Esseger ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
