IsarMathLib 1.24.0: Update to Isabelle2022

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 \{\langle x,x\rangle : x\in X\} is closed in the product topology on X\times X, the fact that the graph of a function into a Hausdorff space is closed in X\times X 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 X one can construct a topology on X 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.

Advertisement

Tags: , , , ,

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com 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: