Commit 2024-05-07 14:07 838141a2

feat(Mathlib/Order/Ideal): ideals of sets are stable under directed unions and chains (#12651) We prove that the directed union of a non-empty directed union of ideals of subsets of a preorder is an ideal, and in particular ideals of subsets of a preorder are stable under unions. In order to prove it, we also add directed_on_sUnion, a variant of directed_on_iUnion.