IsarMathLib 1.22.0: Uniform covers part II

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 $\Theta$ is a family of uniform covers of $X$ then the following collection $\Phi$ of subsets of $X\times X$ is a (diagonal) uniformity:

$\Phi = \{A\in Pow(X\times X): \exists_{P\in \Theta} \bigcup\{U\times U: U\in P\} \subseteq A\}$ .

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 $\Phi$ is a uniformity on $X$ then the following collection of covers of $X$ is a family of uniform covers:

$\{P\in \text{Covers}(X). \exists_{A\in \Phi} \forall_{x\in X} \exists_{U\in P} A\{x \} \subseteq U\}$ .

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.

Other news

Carnegie Mellon received $20 million to establish a Center for Formal Mathematics. The gift was made by Charles C. Hoskinson, the founder of Cardano and co-founder of Ethereum. As one of the Carnegie Mellon officials said

“Charles’ generosity is helping us to make it possible for Lean mathematics to be more predominantly studied and to make it more accessible as an educational tool.”

It looks like “Lean mathematics” is becoming a synonym of “formalized mathematics” in a similar way as “google” has become a synonym of “search engine”. I can’t say I am happy about it.

Timothy Gowers twitted recently:

A. If you have formalized your proof in a language such as Coq or Lean, then you’ve definitely got a proof.

It is good to hear such assurance form a prominent mathematician. I was wandering what would happen if someone from outside of academia solved and important open problem. How helpful would it be to have a formalization to back up their claim in such case? For me a formally verified proof is more trustworthy and carry more weight than any peer reviewed one, but I have had an impression that this opinion is not common among mathematicians.

Tags: formalized mathematics, IsarMathLib releases

This entry was posted on October 5, 2021 at 4:58 pm and is filed under IsarMathLib releases, mathematics. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

Formalized Mathematics