Mathlib Map

Theorems · Definition · category theory

TopCat.carrier

TopCat → Type u

The underlying type.

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

Around this declaration

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

AlgebraicGeometry.Scheme.Opens · cited by 1149Scheme.OpensTopologicalSpace.Opens.map · cited by 645Opens.mapTopCat.Presheaf.stalk · cited by 407Presheaf.stalkTopCat.Presheaf · cited by 371TopCat.PresheafTopCat.Presheaf.germ · cited by 208Presheaf.germAlgebraicGeometry.Scheme.Hom.opensFunctor · cited by 204Hom.opensFunctorAlgebraicGeometry.Scheme.Hom.app · cited by 176Hom.appTopCat.Presheaf.pushforward · cited by 174Presheaf.pushforwardTopCat.Hom.hom · cited by 169Hom.homAlgebraicGeometry.Scheme.basicOpen · cited by 141Scheme.basicOpenAlgebraicGeometry.Scheme.Hom.appLE · cited by 138Hom.appLEAlgebraicGeometry.Scheme.Hom.appTop · cited by 109Hom.appTopAlgebraicGeometry.Scheme.ΓSpecIso · cited by 106Scheme.ΓSpecIsoAlgebraicGeometry.Scheme.homOfLE · cited by 103Scheme.homOfLEAlgebraicGeometry.Scheme.residueField · cited by 95Scheme.residueFieldTopCat · cited by 1889TopCatTopCat.carrierCITED BYCITES

Cites1

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

Cited by4,354

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 4,354.