Theorems · Theorem · general topology
Nat.cofinite_eq_atTop
Filter.cofinite = Filter.atTop
For natural numbers the filters Filter.cofinite and Filter.atTop coincide.
- Defined in
- Mathlib.Order.Filter.Cofinite
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement · cited by 8,121
- Filter.atTopstatement · cited by 2,405
- le_antisymmproof · cited by 2,068
- Set.Finiteproof · cited by 1,814
- Filter.cofinitestatement · cited by 251
- Filter.atTop_basisproof · cited by 42
- Filter.HasBasis.ge_iffproof · cited by 28
- Set.compl_Iciproof · cited by 11
- Set.finite_lt_natproof · cited by 8
- Filter.atTop_le_cofiniteproof · cited by 3
Cited by37
Results whose statement or proof uses this declaration.
- Summable.tendsto_atTop_zeroproof · cited by 10
- Summable.of_norm_bounded_eventually_natproof · cited by 6
- Nat.frequently_atTop_iff_infiniteproof · cited by 5
- Nat.hyperfilter_le_atTopproof · cited by 5
- summable_of_isBigO_natproof · cited by 4
- LieModule.eventually_genWeightSpace_smul_add_eq_botproof · cited by 4
- Filter.IsBoundedUnder.bddBelow_rangeproof · cited by 3
- Filter.IsBoundedUnder.bddAbove_rangeproof · cited by 2
- ENNReal.tendsto_atTop_zero_of_tsum_ne_topproof · cited by 2
- Asymptotics.bound_of_isBigO_nat_atTopproof · cited by 2
- Summable.hasProdUniformlyOn_nat_one_addproof · cited by 2
- Nat.tendsto_iSup_of_tendsto_limsupproof · cited by 2