Theorems · Definition · general topology
CofiniteTopology
Type u_5 → Type u_5
A type synonym equipped with the topology whose open sets are the empty set and the sets with finite complements.
- Defined in
- Mathlib.Topology.Constructions
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- WithTopologyproof · cited by 30
- TopologicalSpace.cofiniteproof · cited by 9
Cited by11
Results whose statement or proof uses this declaration.
- CofiniteTopology.ofstatement · cited by 12
- t1Space_TFAEstatement and proof · cited by 8
- CofiniteTopology.nhds_eqstatement and proof · cited by 2
- OnePoint.not_continuous_cofiniteTopology_of_symmstatement and proof · cited by 1
- CofiniteTopology.continuous_ofstatement · cited by 1
- t1Space_iff_continuous_cofinite_ofstatement · cited by 1
- Continuous.homeoOfEquivCompactToT2.t1_counterexampleproof · cited by 0
- CofiniteTopology.isClosed_iffstatement and proof · cited by 0
- CofiniteTopology.isOpen_iffstatement and proof · cited by 0
- CofiniteTopology.isOpen_iff'statement and proof · cited by 0
- CofiniteTopology.mem_nhds_iffstatement and proof · cited by 0