A new version of Isabelle got released a couple of days ago and this version updates IsarMathLib to Isabelle2022. The Isabelle/ZF logic that IsarMathLib is based on is not actively developed, which has a good side that there are no changes and upgrades like this are easy and problem-free.

There is a little bit of formalized mathematics added in this IsarMathLib release as well. I added a couple of results from general topology that I always considered neat and elegant: a characterization of Hausdorff spaces as those for which the diagonal is closed in the product topology on , the fact that the graph of a function into a Hausdorff space is closed in and that two continuous functions into a Hausdorff space are equal on a closed set.

Another theorem added is related to abstract neighborhood systems. IsarMathLib had had a formalization of the fact that if one has a neighborhood system on one can construct a topology on and vice versa: starting from a topology we can define a natural neighborhood system. In this release I added a theorem asserting that if we start from a neighborhood system, create a topology from it, then create it’s natural neighborhood system, we get back the original neighborhood system.

### Like this:

Like Loading...

*Related*

Tags: formalized mathematics, general topology, Hausdorff spaces, IsarMathLib releases, neighborhood systems

This entry was posted on October 29, 2022 at 7:23 pm and is filed under IsarMathLib releases. 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.

## Leave a Reply