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.
Tags: formalized mathematics, general topology, Hausdorff spaces, IsarMathLib releases, neighborhood systems
Leave a Reply