Mathlib Map

Theorems · Definition · order theory

PartOrd.carrier

PartOrd → Type u_1

The underlying partially ordered type.

Defined in
Mathlib.Order.Category.PartOrd
Cited by
93 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.

PartOrd.Hom.hom · cited by 20Hom.homPartOrd.dual · cited by 13PartOrd.dualBddOrd.Hom.hom · cited by 8Hom.homFinPartOrd.dual · cited by 6FinPartOrd.dualBddOrd.dual · cited by 6BddOrd.dualFinPartOrd.dualEquiv · cited by 4FinPartOrd.dualEquivFinPartOrd.Iso.mk · cited by 4Iso.mkBddOrd.dualEquiv · cited by 2BddOrd.dualEquivPartOrd.Iso.mk · cited by 2Iso.mkBddOrd.Hom.ext · cited by 2Hom.extBddOrd.Hom.hom' · cited by 2Hom.hom'BddOrd.Iso.mk · cited by 2Iso.mkPartOrd.Hom.ext · cited by 2Hom.extPartOrd.Hom.hom' · cited by 2Hom.hom'PartOrd.nerveFunctor · cited by 2PartOrd.nerveFunctorPartOrd · cited by 65PartOrdPartOrd.carrierCITED BYCITES

Cites1

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

  • PartOrdstatement and proof · cited by 65

Cited by131

Results whose statement or proof uses this declaration.