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.
Tags: formalized mathematics, IsarMathLib releases, weirdmath
Leave a Reply