mathlib3

dbbd696d - feat(order/ideal): order ideals, cofinal sets and the Rasiowa-Sikorski lemma (#2850)

feat(order/ideal): order ideals, cofinal sets and the Rasiowa-Sikorski lemma (#2850) 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.