Filters in posets

Stream: Is there code for X?

[Adam Topaz]

Do we have a definition of a filter in an arbitrary poset? @Yaël Dillies ?

[Yaël Dillies]

docs#Order.PFilter, please don't use before this summer I want to refactor it deeply

[Adam Topaz]

Thanks. I'm just looking around for now, not doing anything explicit (yet ;))

[Adam Topaz]

What about ultrafilters?

[Yaël Dillies]

Nope

[Adam Topaz]

ok, thanks

[Floris van Doorn]

Note: we do have docs#Order.PFilter.IsPrime, which I believe is equivalent for lattices.

[Anatole Dedecker]

Yaël Dillies said:

docs#Order.PFilter, please don't use before this summer I want to refactor it deeply

May I add that I would like ideals (of sets, but I can do with the general poset case) as well ? :sweat_smile: