Theorems · Theorem · general topology
Rat.not_countably_generated_cocompact
¬(Filter.cocompact ℚ).IsCountablyGenerated
- Defined in
- Mathlib.Topology.Instances.RatLemmas
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- nhdsproof · cited by 5,554
- Set.rangeproof · cited by 4,705
- Filter.Tendstoproof · cited by 3,814
- Filter.atTopproof · cited by 2,405
- Filter.IsCountablyGeneratedstatement and proof · cited by 220
- Filter.Tendsto.eventuallyproof · cited by 174
- Filter.Eventually.existsproof · cited by 168
- Filter.cocompactstatement and proof · cited by 141
- Filter.tendsto_infproof · cited by 23
- Filter.exists_seq_tendstoproof · cited by 21
- IsCompact.compl_mem_cocompactproof · cited by 13
- Filter.Tendsto.isCompact_insert_rangeproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Rat.not_countably_generated_nhds_infty_opcproof · cited by 1