Mathlib Map

Theorems · Definition · category theory

Preord.carrier

Preord → Type u_1

The underlying preordered type.

Defined in
Mathlib.Order.Category.Preord
Cited by
35 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Preord.Hom.hom · cited by 13Hom.homPreord.dual · cited by 7Preord.dualalexDiscEquivPreord · cited by 6alexDiscEquivPreordpreordToCat · cited by 3preordToCatpreordToPartOrd · cited by 3preordToPartOrdpreordToPartOrdCompToDualIsoToDualCompPreordToPartOrd · cited by 3preordToPartOrdCompToDual…Preord.Iso.mk · cited by 3Iso.mkPreord.Hom.ext · cited by 2Hom.extPreord.Hom.hom' · cited by 2Hom.hom'Preord.dualEquiv · cited by 2Preord.dualEquivPreord.ext · cited by 1Preord.extPreord.hom_ext · cited by 1Preord.hom_extPreord.Hom.casesOn · cited by 0Hom.casesOnPreord.Hom.ext_iff · cited by 0Hom.ext_ifftopToPreord_obj_coe · cited by 0topToPreord_obj_coePreord · cited by 42PreordPreord.carrierCITED BYCITES

Cites1

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

  • Preordstatement and proof · cited by 42

Cited by50

Results whose statement or proof uses this declaration.