Just another WordPress.com weblog
In this release I updated IsarMathLib to the new Isabelle 2025-1. On the mathematics side I continued the story of defining uniformities with collections of psedudometrics. As they say in General Topology Chapter IX §1 no. 4: The significance of defining a uniformity by means of a family of pseudometrics lies in the fact that […]
In this release I edited a theory file about actions of integers on abelian groups (-modules) contributed by Daniel de la Concepción Sáez a couple of years ago so that it is written in Isar dialect supported by the isarmathlib.org site and finished the proof that collection of uniformities on a fixed set, ordered by […]
This release is mostly about recent contributions by Daniel de la Concepción Sáez. There are three theory files added on ultrafilters, ultraproducts, internal sets and hypernatural numbers (i.e. nonnegative hyperintegers). On my side I formalized some material about the order structure on the collection of uniformities on a given set . Such uniformities are collections […]
As in the title I updated IsarMathLib to Isabelle2025 released March 13th. There is quite a lot of new formalized mathematics in this release, scattered over many subjects. One new theory that stands out a bit is about uniformities defined by collections of pseudometrics. In one of previous posts I wrote about how a single […]
The discussion took place at the Hausdorff Center for Mathematics about a month ago. Best of the best had gathered – Mario Carneiro, Georges Gonthier, Peter Koepke, Angeliki Koutsoukou-Argyraki, Laurence Paulson, Josef Urban (the moderator) and some others I did not recognize (a list of participants under that video would be useful). After 1 hour […]
Suppose is a pseudometric and consider the collection of relations on defined by . satisfies the following four conditions: This means that is a fundamental system of entourages and the supersets of (i.e. ) form a uniformity. At this point we have two topologies on : one metric topology coming directly from the pseudometric as […]
This release updates IsarMathLib to Isabelle2024. There are also three new theory files on modules contributed by Daniel de la Concepción Sáez. Modules_ZF_1 covers linear combinations, linear dependency, submodules and spans. The Modules_ZF_2 theory file discusses ideals of a ring as modules and annihilators. In the IntModule_ZF theory file Daniel shows that every abelian group […]
This release adds definitions and basic facts about modules and vector spaces defined as ring (or field) actions on abelian groups. I also edited two theory files contributed earlier by Daniel de la Concepción Sáez (Ring_ZF_2 and Ring_ZF_3) so that they are now included at the isarmathlib.org site. What are ring actions? Let be an […]
A couple of years ago I got a task of writing a module for pricing gamma swaps. I found the task quite difficult, as all I got to base on was an Excel spreadsheet with formulas that were clearly wrong and the few sources on the Internet that I found lacked details. This post (and […]
Following the Isabelle2023 release I have released an updated version of IsarMathLib. This release does not contain new formalized material, but I have edited two old (from around 2013, with some later additions) theory files contributed by Daniel de la Concepción Sáez so that they can be included in the isarmathlib.org site. The first theory […]