The material added in this release is again about uniform spaces, more specifically about the equivalence of defining uniform space through (diagonal) uniformities and through uniform covers. The previous release concluded with the theorem stating that if 
This shows that if we define a uniform space through a family of uniform covers then we can always get the usual definition by transforming that family into a uniformity.
The current release adds the dual fact (unicov_from_uniformity): if
The next two theorems show that these two transformations are inverses of each other.
I should probably quote sources for my formalization so that not to create an impression that I claim I am inventing some new stuff here. However the truth is that I found the Willard’s “General Topology” book that I bought for this nearly useless. So I ended up mostly getting definitions and facts from the “Uniform cover definition” section on the Wikipedia page on uniform spaces, and figuring out the proofs by myself. The only exception was a nice (even if not completely correct) proof that barycentric refinement of a barycentric refinement is a star refinement by Henno Brandsma that I found on Stack Exchange and converted to the bary_bary_star lemma.
. A collection 
of subsets of 
. 
and a collection of 
of subsets of 
in 
.
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 
.
, 
and 
we can find a cover 
that is a star-refinement of both 
is a member of 
.
as 
one needs to find a set 
such that 
(here 
is the composition of relation 
with itself). For that, I found the following identity useful:
if and only if 
and 
. The “if and only if” is worth noting here as this is different from the ordered group definition where one-sided implications are sufficient (I lost a couple of hours working with a wrong definition). 
, then we can define the left and right inverses of a loop element 
as the only solutions to the equations 
and 
. In a loop these inverses do not have to be the same in general. If the loop operation is associative then we get a group and the left and right inverses unify to become the group inverse.
or 
has a unique solution. So, a quasigroup is like a group except we do not require associativity or existence of a neutral element. If we denote those solution as 
and 
respectively we get the identities 
and 
by definition and, with the uniqueness, we get 
and 
, which may serve as an alternative definition of quasigroup. 
being a metric and one stating that the collection of unions of open disks is a topology on reals.
and 
, very important in mathematics based on set theory) were replaced by some placeholder symbol. Errors related to LaTeX are difficult to debug in Isabelle (at least for me), but this time I was lucky. The Isabelle2021 release notes contained information that the “The standard LaTeX engine is now lualatex, according to settings
that satisfies the conditions 
, 
and 
for all 
. This is sufficient to prove that the collection of subsets of 
) is a topology, making this metric space a topological space. If we replace the interval 
in the definition of pseudo-metric by the nonnegative set of a linearly ordered, abelian, Archimedean group then we are not changing anything as such group is isomorphic to a subgroup of the additive group of real numbers. I was curious: what is really needed to get a topological space from a pseudo-metric space this way? Do we really need the group to be Archimedean? Does the group operation have to be commutative? Do we need the order to be total? Amusingly, the answer to these questions is “no”. The group does not have to be abelian and the Archimedean property is not needed. The linear order condition can be relaxed by assuming that the positive set is a meet semi-lattice (every two-element subset has a greatest lower bound) under the group order relation. I don’t know if this is useful to know, but surely my personal curiosity got satisfied.
the set 
is also a subgroup. These theorems turned out not to be in the Mizar Mathematical Library, but Roland Coghetto posted formalization of those 
) semigroups.
