Theorems · Definition · general topology
Ctop.toTopsp
{α : Type u_1} → {σ : Type u_3} → Ctop α σ → TopologicalSpace αEvery Ctop is a topological space.
- Defined in
- Mathlib.Data.Analysis.Topology
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- Set.rangeproof · cited by 4,705
- TopologicalSpace.generateFromproof · cited by 62
- Ctop.fproof · cited by 24
- Ctopstatement and proof · cited by 14
Cited by14
Results whose statement or proof uses this declaration.
- Ctop.toTopsp_isTopologicalBasisstatement · cited by 2
- Ctop.Realizer.eqstatement · cited by 2
- Ctop.mem_nhds_toTopspstatement · cited by 2
- Ctop.Realizer.ext'statement · cited by 1
- Ctop.Realizer.mk.injstatement and proof · cited by 1
- Ctop.Realizer.mk.noConfusionstatement and proof · cited by 1
- Ctop.toRealizerstatement · cited by 0
- Ctop.Realizer.casesOnstatement and proof · cited by 0
- Ctop.Realizer.extstatement · cited by 0
- Ctop.Realizer.noConfusionproof · cited by 0
- Ctop.Realizer.noConfusionTypeproof · cited by 0
- Ctop.Realizer.recOnstatement and proof · cited by 0