Theorems · Definition · general topology
Filter.codiscrete
(X : Type u_3) → [TopologicalSpace X] → Filter X
In any topological space, the open sets with discrete complement form a filter,
defined as the supremum of all punctured neighborhoods.
See Filter.mem_codiscrete' for the equivalence.
- Defined in
- Mathlib.Topology.DiscreteSubset
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 50 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement · cited by 8,121
- Set.univproof · cited by 3,945
- Filter.codiscreteWithinproof · cited by 87
Cited by34
Results whose statement or proof uses this declaration.
- IsDiscrete.iUnionproof · cited by 3
- circleMap_preimage_codiscretestatement · cited by 3
- mem_codiscretestatement · cited by 2
- mem_codiscrete'statement · cited by 2
- mem_codiscrete_subtype_iff_mem_codiscreteWithinstatement · cited by 2
- compl_mem_codiscrete_iffstatement · cited by 2
- codiscrete_le_cofinitestatement and proof · cited by 2
- Set.Finite.compl_mem_codiscretestatement · cited by 2
- Set.Infinite.of_accPtproof · cited by 2
- MeromorphicOn.codiscrete_setOfPred_meromorphicOrderAt_eq_zero_or_topstatement · cited by 2
- Topology.IsEmbedding.image_mem_codiscreteWithin_rangestatement and proof · cited by 1
- AnalyticOnNhd.preimage_zero_mem_codiscretestatement · cited by 1