Commit 2024-01-04 18:16 561e9afe

feat(Order/Filter) : add 2 constructors (#9200) Add two constructors to create filters from a property on sets:

• Filter.comk if the property is stable under finite unions and set shrinking.
• Filter.ofCountableUnion if the property is stable under countable unions and set shrinking Filter.comk is the key ingredient in IsCompact.induction_on but may be convenient to have as individual building block. A Filter generated by Filter.ofCountableUnion is a CountableInterFilter, which is given by the instance Filter.countableInter_ofCountableUnion.

Other changes

• Use Filter.comk for Filter.cofinite, Bornology.ofBounded and MeasureTheory.Measure.cofinite.
• Use Filter.ofCountableUnion for MeasureTheory.Measure.ae.
• Use {_ : Bornology _} instead of [Bornology _] in some lemmas so that rw/simp work with non-instance bornologies.