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.

Formalized Mathematics

IsarMathLib 1.7.4

Leave a Reply Cancel reply

Formalized Mathematics

IsarMathLib 1.7.4

Share this:

Like this:

Related

Leave a Reply Cancel reply