IsarMathLib 1.7.4

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 (x_0, x_1, ..., x_{n-1}) \mapsto \sum_{i=0}^{n-1}x_i is continuous on G^n where (G,+) 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 (\emptyset\rightarrow X) = \{\emptyset\}. Let me explain what this notation means. The A\rightarrow B expression is the set of functions whose domain is A and values belong to B. When we write f:A\rightarrow B we are using the semicolon instead of the usual \in symbol to express the fact that the function f belongs to that set of functions. In particular  \emptyset\rightarrow X is the set of X-valued functions whose domain is the empty set. Well, are there any such functions? In other words is  it true that (\emptyset\rightarrow X) =\emptyset ? 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 x\in \emptyset the value of that function on x is in whatever? So, really \emptyset :\emptyset \rightarrow X. Since the empty set is the only function whose domain is empty, we get (\emptyset\rightarrow X) = 1.  And it’s not a typo, because in ZF \{\emptyset\} 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 X^n where X is (the carrier of) a topological space with topology \tau. Dealing with cartesian products of n sets is somewhat inconvenient in Isabelle/ZF, so I decided to use the space of sequences n\rightarrow X as a proxy for the cartesian product X\times X\times ...\times X (recall that in ZF if n is a natural number, then n = \{ 0, 1,...,n-1\}). Once we talk about topologies on function spaces, why not just define a topology on I\rightarrow X where I is an arbitrary index set? So this is what I did.

To do that I needed to define a base of that topology on I\rightarrow X. 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 N\subseteq I and a function W:N\rightarrow \tau whose values are open sets. Then we can define a set in the base as

B(N,W) = \{ f:I\rightarrow X | \forall_{i\in N} f(i) \in W(i)\}.

The base is then the collection of all such sets B(N,W).

Now we want to show that the whole function space I\rightarrow X is one of the base sets. This corresponds to placing no restrictions on the functions, i.e. we want to have N=\emptyset. This way we start thinking what \emptyset \rightarrow \tau may be.


Tags: , ,

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: