I have released version 1.7.4 of IsarMathLib. The new formal math there is a mostly in the Topology_ZF_3 theory about topologies on function spaces. This is needed to show that the function is continuous on where is a topological group. This will be my goal for the next release.
I am happy to report that I use Isabelle2012 Makarius Wenzel’s Prover IDE for writing formal math and it works very well for me. A screenshot follows.
An amusing fact that I encountered while proving one of the lemmas was that . Let me explain what this notation means. The expression is the set of functions whose domain is and values belong to . When we write we are using the semicolon instead of the usual symbol to express the fact that the function belongs to that set of functions. In particular is the set of -valued functions whose domain is the empty set. Well, are there any such functions? In other words is it true that ? Turns out that the empty set itself satisfies the definition of what it means to be a function (in ZF) and of course the domain of that function is empty. And who can deny that for all the value of that function on is in whatever? So, really . Since the empty set is the only function whose domain is empty, we get . And it’s not a typo, because in ZF is the same as the natural number 1.
Usually such facts are only a source of fun and games, but this one actually did get used in a proof of one of the theorems in the theory added in this release. Here is how it came about.
I needed to have the product topology defined on where is (the carrier of) a topological space with topology . Dealing with cartesian products of sets is somewhat inconvenient in Isabelle/ZF, so I decided to use the space of sequences as a proxy for the cartesian product (recall that in ZF if is a natural number, then ). Once we talk about topologies on function spaces, why not just define a topology on where is an arbitrary index set? So this is what I did.
To do that I needed to define a base of that topology on . The standard approach to define a base for a product topology is by taking all finite products of open sets. In the function space approach this corresponds to taking a finite subset and a function whose values are open sets. Then we can define a set in the base as
The base is then the collection of all such sets .
Now we want to show that the whole function space is one of the base sets. This corresponds to placing no restrictions on the functions, i.e. we want to have . This way we start thinking what may be.