There are three approaches to defining uniform spaces. The first one, through *diagonal* *uniformities* is presented in IsarMathLib in the UniformSpace_ZF theory. This release adds a theory about defining uniform spaces through *uniform covers*.

Consider a set with its powerset (the set of subsets) . A collection of subsets of whose union is equal to is called a *cover* of . So, we can define the set .

For a set and a collection of of subsets of we can define the *star* of *in* as .

For two covers we say that the cover is a star-refinement of the cover and write if for every we can find a such that is contained in .

Finally we are able to define uniform covers. This notion is a bit tricky as there is really no separate notion of a uniform cover. If we look at cover of we cannot say if this is a uniform cover or not. What actually is defined is a *family* of uniform covers. A member of such family can only be called a uniform cover if it is clear from the context what family of uniform covers it belongs to.

A nonempty collection of covers of is called a *family of uniform covers* iff the following two conditions hold:

a) If , and , then

b) For every two covers we can find a cover that is a star-refinement of both and

This definition is slightly different that the one on the Wikipedia page on uniform spaces, which specifically requires that the trivial cover is a member of . However, since every cover is a star-refinement of the trivial cover and is not empty, condition a) implies that .

The key fact here is that if is a family of uniform covers of then the following collection of subsets of is a (diagonal) uniformity:

In words, is the collection of supersets of sets of the form as ranges over .

In Willard’s “General Topology” book the proof that is a uniformity is left as a “straightforward exercise” for the reader. Typically that means that the proof is long and tedious and the author does not feel like typing all that down. In this case the proof is indeed of mostly straightforward “follow your nose” kind right up to the moment when given a set one needs to find a set such that (here is the composition of relation with itself). For that, I found the following identity useful:

It took me some effort to figure out this identity and I was ready to type the proof of that in Isabelle, split into two inclusions etc. To my amazement though Isabelle accepted this fact without an explicit proof, only with the reference to the definition of star. This was probably the most unclear to me fact that was obvious to Isabelle that I have seen writing proofs for IsarMathLib so far. I left the proof of this identity as an exercise for the reader. This time the straightforwardness of this fact got certified by Isabelle.

Which brings us to the subject of

## Automation in proof assistants

Read the rest of this entry »