Commit 2024-03-28 18:15 485ed3cc

View on Github →

feat : define CardinalInterFilter (#10531) CardinalInterFilter generalizes CountableInterFilter to allow for a specific cardinality, where the filter must be stable under intersections over a number of sets lower than this cardinality. Prepares the way for K-Lindelöf spaces.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/CardinalInter.lean

added theorem CardinalInterFilter.of_CardinalInterFilter_of_lt

added theorem CardinalInterFilter.toCountableInterFilter

added theorem Filter.EventuallyEq.cardinal_bInter

added theorem Filter.EventuallyEq.cardinal_bUnion

added theorem Filter.EventuallyEq.cardinal_iInter

added theorem Filter.EventuallyEq.cardinal_iUnion

added theorem Filter.EventuallyLE.cardinal_bInter

added theorem Filter.EventuallyLE.cardinal_bUnion

added theorem Filter.EventuallyLE.cardinal_iInter

added theorem Filter.EventuallyLE.cardinal_iUnion

added theorem Filter.cardinalInterFilter_aleph0

added theorem Filter.cardinal_bInter_mem

added theorem Filter.cardinal_iInter_mem

added theorem Filter.eventually_cardinal_ball

added theorem Filter.eventually_cardinal_forall

added theorem cardinalInterFilter_aleph_one_iff

added theorem cardinal_sInter_mem

Modified Mathlib/Order/Filter/CountableInter.lean