I struggle with understanding the definition of topological filter provided in Filter.thy . My explaination of the problem is a little involved so in order to avoid cluttering zulip with code blocks, I posted a stack-overflow question (it will also be easier to find by google search in the future).

https://stackoverflow.com/questions/75120033/topological-filters-in-isabelle

In short, the axioms of topological filter don't match with those typically found in textbooks and it seems that the Isabelle's definition is actually not equivalent to them. Moreover, the notation is quite convoluted so maybe I understood something wrong.

Is there somebody interested in enlightening me?

Unfortunately I am of no help here but I would like to thank you for this example. Now when someone asks why I prefer to formalize mathematics in Isabelle/ZF rather than Isabelle/HOL I can point to the definition of filter in this StackOverflow question and the one in IsarMathLib.

You did get an answer on StackOverflow and I also commented on it. I just wanted to add that some of the confusion probably stems from the fact that filters are defined with predicates instead of with sets. I honestly have no idea why that is the case and e.g. Lean does it differently, if I recall correctly. One possibility is that filters were formalised back in the period when Isabelle/HOL didn't have a set type but rather did everything with predicates (`'a ⇒ bool`

) and filters were never changed to sets.

If you translate all the filter definitions to sets in your head, they might become more intuitive.

Last updated: Dec 07 2023 at 16:21 UTC