Mathlib Map

Theorems · Definition · category theory

CompHausLike.toTop

{P : TopCat → Prop} → CompHausLike P → TopCat

The underlying topological space of an object of CompHausLike P.

Defined in
Mathlib.Topology.Category.CompHausLike.Basic
Cited by
258 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ProfiniteGrp.limit · cited by 23ProfiniteGrp.limitProfiniteGrp.Hom.hom · cited by 20Hom.homProfiniteGrp.limitConePtAux · cited by 19ProfiniteGrp.limitConePtA…CompHausLike.preregular · cited by 19CompHausLike.preregularProfiniteAddGrp.Hom.hom · cited by 16Hom.homCompHausLike.HasExplicitPullback · cited by 14CompHausLike.HasExplicitP…CompHausLike.finiteCoproduct · cited by 13CompHausLike.finiteCoprod…CompHausLike.pullback · cited by 13CompHausLike.pullbackCompHausLike.const · cited by 12CompHausLike.constCompHausLike.LocallyConstant.functorToPresheaves · cited by 11LocallyConstant.functorTo…CompHausLike.LocallyConstant.functor · cited by 11LocallyConstant.functorProfiniteGrp.diagram · cited by 10ProfiniteGrp.diagramCompHausLike.compHausLikeToTop · cited by 10CompHausLike.compHausLike…Profinite.asLimitCone · cited by 8Profinite.asLimitConeProfinite.diagram · cited by 8Profinite.diagramTopCat · cited by 1889TopCatCompHausLike · cited by 145CompHausLikeCompHausLike.toTopCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • TopCatstatement and proof · cited by 1,889
  • CompHausLikestatement and proof · cited by 145

Cited by409

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 409.