Stream: General

Topic: Definition of topological filters


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 12:28 UTC