Theorems · Definition · general topology
Filter.cofinite
{α : Type u_2} → Filter αThe cofinite filter is the filter of subsets whose complements are finite.
- Defined in
- Mathlib.Order.Filter.Cofinite
- Cited by
- 251 results in Mathlib
- Foundations
- Depth 65 from the axioms, rests on 1,251 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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.Finiteproof · cited by 1,814
- Set.Finite.subsetproof · cited by 285
- Set.Finite.unionproof · cited by 74
- Set.finite_emptyproof · cited by 26
- Filter.comkproof · cited by 6
Cited by270
Results whose statement or proof uses this declaration.
- Nat.cofinite_eq_atTopstatement · cited by 37
- Filter.hyperfilterproof · cited by 30
- RestrictedProduct.singlestatement · cited by 18
- RestrictedProduct.mulSinglestatement · cited by 16
- Summable.tendsto_cofinite_zerostatement · cited by 16
- Set.Finite.compl_mem_cofinitestatement · cited by 14
- Summable.of_norm_bounded_eventuallystatement and proof · cited by 13
- Function.Injective.tendsto_cofinitestatement and proof · cited by 9
- IsDedekindDomain.FiniteAdeleRingproof · cited by 9
- MvPowerSeries.IsRestrictedproof · cited by 8
- summable_of_isBigOstatement and proof · cited by 8
- Int.cofinite_eqstatement · cited by 7
Showing the 200 most cited of 270.