Commit 2024-04-25 07:45 f1d422f4

View on Github →

Feat: Define cocardinal and cocountable filters (#11774) Define the cocardinal and cocountable filters as those consisting of sets whose complements have a given cardinality/ are countable.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Cocardinal.lean

added def Filter.cocardinal

added theorem Filter.cocardinal_aleph0_eq_cofinite

added theorem Filter.cocardinal_inf_principal_neBot_iff

added theorem Filter.compl_mem_cocardinal_of_card_lt

added theorem Filter.eventually_cocardinal

added theorem Filter.eventually_cocardinal_ne

added theorem Filter.eventually_cocardinal_nmem_of_card_lt

added theorem Filter.frequently_cocardinal

added theorem Filter.frequently_cocardinal_mem

added theorem Filter.hasBasis_cocardinal

added theorem Filter.mem_cocardinal

added theorem Filter.mem_cocountable

added theorem Finset.eventually_cocardinal_nmem

added theorem Set.Finite.compl_mem_cocardinal