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 »