Theorems · Definition · general topology
Filter.cocompact
(X : Type u_1) → [TopologicalSpace X] → Filter X
Filter.cocompact is the filter generated by complements to compact sets.
- Defined in
- Mathlib.Topology.Defs.Filter
- Cited by
- 141 results in Mathlib
- Foundations
- Depth 50 from the axioms, rests on 544 definitions · uses propext, Quot.sound
- Assumes
- TopologicalSpace
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
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement · cited by 8,121
- Compl.complproof · cited by 2,925
- iInfproof · cited by 1,690
- IsCompactproof · cited by 1,282
- Filter.principalproof · cited by 740
Cited by157
Results whose statement or proof uses this declaration.
- MeasureTheory.IsTightMeasureSetproof · cited by 31
- Filter.hasBasis_cocompactstatement · cited by 14
- Filter.mem_cocompactstatement · cited by 14
- IsCompact.compl_mem_cocompactstatement · cited by 13
- Topology.IsClosedEmbedding.tendsto_cocompactstatement · cited by 9
- Metric.cobounded_eq_cocompactstatement · cited by 8
- MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_leproof · cited by 7
- Filter.cocompact_eq_cofinitestatement · cited by 7
- Filter.comap_cocompact_lestatement · cited by 7
- cocompact_eq_atBot_atTopstatement · cited by 6
- tendsto_norm_cocompact_atTopstatement · cited by 6
- Filter.coclosedCompact_eq_cocompactstatement · cited by 5