Theorems · Inductive type · general topology
DiscreteQuotient
(X : Type u_5) → [TopologicalSpace X] → Type u_5
The type of discrete quotients of a topological space.
- Defined in
- Mathlib.Topology.DiscreteQuotient
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
Cited by93
Results whose statement or proof uses this declaration.
- DiscreteQuotient.toSetoidstatement and proof · cited by 45
- DiscreteQuotient.projstatement and proof · cited by 23
- DiscreteQuotient.ofLEstatement and proof · cited by 14
- DiscreteQuotient.LEComapstatement and proof · cited by 12
- DiscreteQuotient.mapstatement and proof · cited by 9
- Profinite.asLimitConestatement and proof · cited by 8
- Profinite.diagramstatement · cited by 8
- DiscreteQuotient.LEComap.monostatement and proof · cited by 4
- DiscreteQuotient.proj_surjectivestatement and proof · cited by 4
- LightProfinite.toLightDiagramproof · cited by 3
- Condensed.isColimitLocallyConstantPresheafDiagramstatement · cited by 3
- DiscreteQuotient.comapstatement and proof · cited by 3