Theorems · Definition · general topology
Filter.cocardinal
(α : Type u) → {c : Cardinal.{u}} → c.IsRegular → Filter αThe filter defined by all sets that have a complement with at most cardinality c. For a union
of c sets of c elements to have c elements, we need that c is a regular cardinal.
- Defined in
- Mathlib.Order.Filter.Cocardinal
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Filterstatement · cited by 8,121
- Set.Elemproof · cited by 7,166
- Set.ofPredproof · cited by 6,101
- Cardinalstatement and proof · cited by 2,598
- Cardinal.mkproof · cited by 942
- Cardinal.IsRegularstatement and proof · cited by 282
- Filter.ofCardinalUnionproof · cited by 1
Cited by14
Results whose statement or proof uses this declaration.
- Filter.frequently_cocardinalstatement · cited by 2
- Filter.compl_mem_cocardinal_of_card_ltstatement · cited by 2
- Filter.mem_cocardinalstatement · cited by 2
- Filter.eventually_cocardinal_notMem_of_card_ltstatement · cited by 1
- Filter.cocountableproof · cited by 1
- Filter.frequently_cocardinal_memstatement · cited by 0
- Filter.cocardinal.congr_simpstatement and proof · cited by 0
- Filter.eventually_cocardinalstatement · cited by 0
- Filter.eventually_cocardinal_nestatement · cited by 0
- Filter.hasBasis_cocardinalstatement and proof · cited by 0
- Finset.eventually_cocardinal_notMemstatement · cited by 0
- Filter.cocardinal_aleph0_eq_cofinitestatement · cited by 0