[Merged by Bors] - feat(order/ideal): order ideals, cofinal sets and the Rasiowa-Sikorski lemma

[dwarn]

We define order ideals and cofinal sets, and use them to prove the (very simple) Rasiowa-Sikorski lemma: given a countable family of cofinal subsets of an inhabited preorder, there is an upwards directed set meeting each one. This provides an API for certain recursive constructions.

[dwarn]

The predicates downwards_closed and cofinal maybe belong in order.basic? There is unbounded in order.basic, which claims to mean cofinal, but it's not quite what we want.

[dwarn]

To be clear I don't expect anyone to know what Rasiowa-Sikorski says -- I didn't know this name until I looked it up recently, and it only seems to be used in the context of "forcing with countable transitive models". So I definitely would like this file to be accessible to people who have never heard of the lemma!

Would it be better to use descriptive names here? Something like generic_cofilter_of_countable_cofinal instead of 'rasiowa_sikorski'? Cofilter is a made-up term for the order-theoretic dual notion of 'filter' (which afaics only exists in mathlib specialized to the power set?), i.e. by cofilter I mean a downwards closed, upwards directed set.

[jcommelin]

Yes, please use descriptive names (and mention Namey-names in the docstrings).

[dwarn]

It's all descriptive names now, but they may or may not make sense.

I wrote up a proof of BCT to illustrate the usage of this: link to zulip

[urkud]

Since you're talking about cofilters here, does it make sense to formulate this using filter.frequently? It seems that cofinal is exactly ∃^f x in at_top, p x.

[dwarn]

It seems like filter.frequently_at_top relates cofinal with at_top, but it needs assumptions on the preorder that are not true here. In particular, the preorder in this file is most likely not directed -- i.e. there can be 'incompatible' pairs of elements -- and at_top is most likely the improper filter.

From reading Wikipedia it seems that the correct term for what I've referred to as 'cofilter' is 'order ideal' - I'll change the names in this file accordingly. It should be noted that a "filter on P" in mathlib's sense (i.e. something like at_top) is nothing like an order ideal on P: a filter on P is rather an order ideal on set P ordered by reverse inclusion. In practice, P is often represented as a subtype of some set A, and then the order ideal on P induces a filter on A. There is probably more to be said here to relate order ideals on P with filters on A...

[urkud]

Thank you for the explanation. I saw "cofilter" and started thinking how to relate this to filters. One more comment about names: I think that using name "generic" in a rarely used lemma is not a good idea because we won't be able to reuse this name in other files.

BTW, I think that without a directed assumption ∃^f x in at_top, p x is equivalent to ∀ (s : set α), finite s → ∃ x ∈ upper_bounds s, p x. Not sure if this is good for your case.

[robertylewis]

@urkud are you happy with the current state here? (Just asking because you were commenting earlier.) This looks fine to me.

[urkud]

LGTM

[urkud]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs