IsarMathLib version 1.13.0: Roelcke uniformity

I have released version 1.13.0 of IsarMathLib. This release adds the definition and basic properties of the Roelcke uniformity, contributed by Daniel de la Concepción Sáez.

So, what is Roelcke uniformity? As we all know each topological group is a uniform space with two natural uniformities: the left uniformity and right uniformity. The collection of uniformities on a set forms a lattice (in fact, a complete one) so it is natural to ask what are the meet and join of the left and right uniformities. The meet is called the Roelcke uniformity. More details with references can be found in answers to this StackExchange question and the formalization is available in the IsarMathLib’s TopologicalGroup_Uniformity_ZF theory.



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 )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: