Aleksander Mendoza-Drosik (Jan 14 2023 at 17:49): Aleksander Mendoza-Drosik (Jan 14 2023 at 17:49):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?
Sławomir Kołodyńaski (Jan 14 2023 at 20:01):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.
Manuel Eberl (Jan 15 2023 at 12:01):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.
Manuel Eberl (Jan 15 2023 at 12:02):If you translate all the filter definitions to sets in your head, they might become more intuitive.
Last updated: Dec 21 2024 at 12:33 UTC